More twicks on hash-consing

 - When hash-consing, seeing ident as having string as sub-structure
   induces a penalty: two searchs are done in two tables
   (one for string, one for id).
   We simply say now that the hcons function for ident is the one
   for string

 - use more == during hash-consing of Names.uniq_ident and
   Names.module_path

 - clarification concerning hash-cons of Names.constant and
   Names.mutual_inductive: we only hash-cons the canonical part,
   but == could be used nonetheless on the obtained pair. Simply
   note that canonical_con of hash-consed constants will produce
   kernel_names that may be (=) but not (==).

 - Code cleanup : no direct use of string hash-consing apart in Names,
   we hence simplify hcons_names

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14464 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions