Default hashconsing of identifiers.

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

1 files changed, 7 insertions, 2 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index d2c06104b..520a9aa64 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -22,6 +22,8 @@ open Pp
 open Errors
 open Util
 
+let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.generate ()
+
 (** {6 Identifiers } *)
 
 type identifier = string
@@ -33,7 +35,11 @@ let check_ident_soft x =
 let check_ident x =
   Option.iter (fun (_,x) -> Errors.error x) (Unicode.ident_refutation x)
 
-let id_of_string s = check_ident_soft s; String.copy s
+let id_of_string s =
+  let () = check_ident_soft s in
+  let s = String.copy s in
+  hcons_string s
+
 let string_of_id id = String.copy id
 
 let id_ord (x:string) (y:string) =
@@ -452,7 +458,6 @@ module Hconstruct = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.generate ()
 let hcons_ident = hcons_string
 let hcons_name = Hashcons.simple_hcons Hname.generate hcons_ident
 let hcons_dirpath = Hashcons.simple_hcons Hdir.generate hcons_ident