Merge with CEDET upstream (rev. 8499).