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

1 files changed, 1 insertions, 2 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 68fbd1807..aa9a55abc 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -631,8 +631,7 @@ val hcons_constr:
   (mutual_inductive -> mutual_inductive) *
   (dir_path -> dir_path) *
   (name -> name) *
-  (identifier -> identifier) *
-  (string -> string)
+  (identifier -> identifier)
   ->
     (constr -> constr) *
     (types -> types)