Modulification of name

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

1 files changed, 42 insertions, 23 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index c6f5f891c..12df0a3c8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -74,16 +74,46 @@ struct
 
 end
 
+
+module Name =
+struct
+  type t = Name of Id.t | Anonymous
+
+  let equal n1 n2 = match n1, n2 with
+  | Anonymous, Anonymous -> true
+  | Name id1, Name id2 -> String.equal id1 id2
+  | _ -> false
+
+  module Self_Hashcons =
+    struct
+      type _t = t
+      type t = _t
+      type u = Id.t -> Id.t
+      let hashcons hident = function
+        | Name id -> Name (hident id)
+        | n -> n
+      let equal n1 n2 =
+        n1 == n2 ||
+        match (n1,n2) with
+          | (Name id1, Name id2) -> id1 == id2
+          | (Anonymous,Anonymous) -> true
+          | _ -> false
+      let hash = Hashtbl.hash
+    end
+
+  module Hname = Hashcons.Make(Self_Hashcons)
+
+  let hcons = Hashcons.simple_hcons Hname.generate Id.hcons
+
+end
+
+type name = Name.t = Name of Id.t | Anonymous
+(** Alias, to import constructors. *)
+
 (** {6 Various types based on identifiers } *)
 
-type name = Name of Id.t | Anonymous
 type variable = Id.t
 
-let name_eq n1 n2 = match n1, n2 with
-| Anonymous, Anonymous -> true
-| Name id1, Name id2 -> String.equal id1 id2
-| _ -> false
-
 type module_ident = Id.t
 
 module ModIdmap = Id.Map
@@ -448,22 +478,6 @@ let eq_egr e1 e2 = match e1, e2 with
 
 (** {6 Hash-consing of name objects } *)
 
-module Hname = Hashcons.Make(
-  struct
-    type t = name
-    type u = Id.t -> Id.t
-    let hashcons hident = function
-      | Name id -> Name (hident id)
-      | n -> n
-    let equal n1 n2 =
-      n1 == n2 ||
-      match (n1,n2) with
-	| (Name id1, Name id2) -> id1 == id2
-        | (Anonymous,Anonymous) -> true
-        | _ -> false
-    let hash = Hashtbl.hash
-  end)
-
 module Hmod = Hashcons.Make(
   struct
     type t = module_path
@@ -526,7 +540,6 @@ module Hconstruct = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-let hcons_name = Hashcons.simple_hcons Hname.generate Id.hcons
 let hcons_mp =
   Hashcons.simple_hcons Hmod.generate (Dir_path.hcons,MBId.hcons,String.hcons)
 let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,Dir_path.hcons,String.hcons)
@@ -631,3 +644,9 @@ let label_of_id = Label.of_id
 let eq_label = Label.equal
 
 (** / End of compatibility layer for [Label] *)
+
+(** Compatibility layer for [Name] *)
+
+let name_eq = Name.equal
+
+(** / End of compatibility layer for [Name] *)