Modulification of name

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

1 files changed, 22 insertions, 7 deletions

diff --git a/kernel/names.mli b/kernel/names.mli
index 947b9e3fde..a51ac0ad86 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -55,14 +55,25 @@ sig
 
 end
 
-(** {6 Various types based on identifiers } *)
+module Name :
+sig
+  type t = Name of Id.t | Anonymous
+  (** A name is either undefined, either an identifier. *)
+
+  val equal : t -> t -> bool
+  (** Equality over names. *)
+
+  val hcons : t -> t
+  (** Hashconsing over names. *)
 
-type name = Name of Id.t | Anonymous
+end
+
+(** {6 Type aliases} *)
+
+type name = Name.t = Name of Id.t | Anonymous
 type variable = Id.t
 type module_ident = Id.t
 
-val name_eq : name -> name -> bool
-
 (** {6 Directory paths = section names paths } *)
 
 module Dir_path :
@@ -100,8 +111,6 @@ sig
 
 end
 
-module ModIdmap : Map.S with type key = module_ident
-
 (** {6 Names of structure elements } *)
 
 module Label :
@@ -164,6 +173,8 @@ sig
 
 end
 
+module ModIdmap : Map.S with type key = module_ident
+
 (** {6 The module part of the kernel name } *)
 
 type module_path =
@@ -290,7 +301,6 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
 
 (** {6 Hash-consing } *)
 
-val hcons_name : name -> name
 val hcons_con : constant -> constant
 val hcons_mind : mutual_inductive -> mutual_inductive
 val hcons_ind : inductive -> inductive
@@ -439,3 +449,8 @@ val string_of_mbid : mod_bound_id -> string
 
 val debug_string_of_mbid : mod_bound_id -> string
 (** @deprecated Same as [MBId.debug_to_string]. *)
+
+(** {5 Names} *)
+
+val name_eq : name -> name -> bool
+(** @deprecated Same as [Name.equal]. *)