Modulification of identifier

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

24 files changed, 157 insertions, 157 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 7d85b362a..1f6c8eeeb 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -24,7 +24,7 @@ open Mod_subst
 let cst_ord k1 k2 = kn_ord (canonical_con k1) (canonical_con k2)
 
 type context_object =
-  | Variable of identifier (* A section variable or a Let definition *)
+  | Variable of Id.t (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
   | Opaque of constant     (* An opaque constant. *)
   | Transparent of constant
@@ -35,7 +35,7 @@ struct
   type t = context_object
   let compare x y =
       match x , y with
-      | Variable i1 , Variable i2 -> id_ord i1 i2
+      | Variable i1 , Variable i2 -> Id.compare i1 i2
       | Axiom k1 , Axiom k2 -> cst_ord k1 k2
       | Opaque k1 , Opaque k2 -> cst_ord k1 k2
       | Transparent k1 , Transparent k2 -> cst_ord k1 k2
diff --git a/library/assumptions.mli b/library/assumptions.mli
index e5d2a977c..f91412013 100644
--- a/library/assumptions.mli
+++ b/library/assumptions.mli
@@ -13,7 +13,7 @@ open Environ
 (** A few declarations for the "Print Assumption" command
     @author spiwack *)
 type context_object =
-  | Variable of identifier  (** A section variable or a Let definition *)
+  | Variable of Id.t  (** A section variable or a Let definition *)
   | Axiom of constant       (** An axiom or a constant. *)
   | Opaque of constant      (** An opaque constant. *)
   | Transparent of constant (** A transparent constant *)
diff --git a/library/declare.ml b/library/declare.ml
index 9d986d185..b5670a1a2 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -80,7 +80,7 @@ let discharge_variable (_,o) = match o with
   | Inl _ -> Some o
 
 type variable_obj =
-    (Univ.constraints, identifier * variable_declaration) union
+    (Univ.constraints, Id.t * variable_declaration) union
 
 let inVariable : variable_obj -> obj =
   declare_object { (default_object "VARIABLE") with
diff --git a/library/declare.mli b/library/declare.mli
index 9cc6e371c..09bd6ac8b 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -55,11 +55,11 @@ type internal_flag =
   | UserVerbose
 
 val declare_constant :
- ?internal:internal_flag -> identifier -> constant_declaration -> constant
+ ?internal:internal_flag -> Id.t -> constant_declaration -> constant
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  identifier -> ?types:constr -> constr -> constant
+  Id.t -> ?types:constr -> constr -> constant
 
 (** [declare_mind me] declares a block of inductive types with
    their constructors in the current section; it returns the path of
@@ -76,11 +76,11 @@ val add_cache_hook : (full_path -> unit) -> unit
 
 (** Declaration messages *)
 
-val definition_message : identifier -> unit
-val assumption_message : identifier -> unit
-val fixpoint_message : int array option -> identifier list -> unit
-val cofixpoint_message : identifier list -> unit
+val definition_message : Id.t -> unit
+val assumption_message : Id.t -> unit
+val fixpoint_message : int array option -> Id.t list -> unit
+val cofixpoint_message : Id.t list -> unit
 val recursive_message : bool (** true = fixpoint *) ->
-  int array option -> identifier list -> unit
+  int array option -> Id.t list -> unit
 
-val exists_name : identifier -> bool
+val exists_name : Id.t -> bool
diff --git a/library/declaremods.ml b/library/declaremods.ml
index b8dd671cf..b58b355f7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -436,7 +436,7 @@ let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
   | [] -> () | _ -> anomaly "Unexpected functor objects" in
   let rec replace_idl = function
     | _,[] -> []
-    | id::idl,(id',obj)::tail when id_eq id id' ->
+    | id::idl,(id',obj)::tail when Id.equal id id' ->
       if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!";
       let substobjs = match idl with
       | [] ->
diff --git a/library/declaremods.mli b/library/declaremods.mli
index dedb9b67a..e52e2620a 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -64,14 +64,14 @@ val declare_module :
   (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
-  identifier ->
-  (identifier located list * ('modast annotated)) list ->
+  Id.t ->
+  (Id.t located list * ('modast annotated)) list ->
   ('modast annotated) module_signature ->
   ('modast annotated) list -> module_path
 
 val start_module : (env -> 'modast -> module_struct_entry) ->
-  bool option -> identifier ->
-  (identifier located list * ('modast annotated)) list ->
+  bool option -> Id.t ->
+  (Id.t located list * ('modast annotated)) list ->
   ('modast annotated) module_signature -> module_path
 
 val end_module : unit -> module_path
@@ -82,14 +82,14 @@ val end_module : unit -> module_path
 
 val declare_modtype : (env -> 'modast -> module_struct_entry) ->
   (env -> 'modast -> module_struct_entry * bool) ->
-  identifier ->
-  (identifier located list * ('modast annotated)) list ->
+  Id.t ->
+  (Id.t located list * ('modast annotated)) list ->
   ('modast annotated) list ->
   ('modast annotated) list ->
   module_path
 
 val start_modtype : (env -> 'modast -> module_struct_entry) ->
-  identifier -> (identifier located list * ('modast annotated)) list ->
+  Id.t -> (Id.t located list * ('modast annotated)) list ->
   ('modast annotated) list -> module_path
 
 val end_modtype : unit -> module_path
diff --git a/library/decls.ml b/library/decls.ml
index af6ee3448..205e51f9b 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -20,25 +20,25 @@ open Libnames
 type variable_data =
     dir_path * bool (* opacity *) * Univ.constraints * logical_kind
 
-let vartab = ref (Idmap.empty : variable_data Idmap.t)
+let vartab = ref (Id.Map.empty : variable_data Id.Map.t)
 
 let _ = Summary.declare_summary "VARIABLE"
   { Summary.freeze_function = (fun () -> !vartab);
     Summary.unfreeze_function = (fun ft -> vartab := ft);
-    Summary.init_function = (fun () -> vartab := Idmap.empty) }
+    Summary.init_function = (fun () -> vartab := Id.Map.empty) }
 
-let add_variable_data id o = vartab := Idmap.add id o !vartab
+let add_variable_data id o = vartab := Id.Map.add id o !vartab
 
-let variable_path id = let (p,_,_,_) = Idmap.find id !vartab in p
-let variable_opacity id = let (_,opaq,_,_) = Idmap.find id !vartab in opaq
-let variable_kind id = let (_,_,_,k) = Idmap.find id !vartab in k
-let variable_constraints id = let (_,_,cst,_) = Idmap.find id !vartab in cst
+let variable_path id = let (p,_,_,_) = Id.Map.find id !vartab in p
+let variable_opacity id = let (_,opaq,_,_) = Id.Map.find id !vartab in opaq
+let variable_kind id = let (_,_,_,k) = Id.Map.find id !vartab in k
+let variable_constraints id = let (_,_,cst,_) = Id.Map.find id !vartab in cst
 
 let variable_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
   make_qualid dir id
 
-let variable_exists id = Idmap.mem id !vartab
+let variable_exists id = Id.Map.mem id !vartab
 
 (** Datas associated to global parameters and constants *)
 
diff --git a/library/decls.mli b/library/decls.mli
index d06db6e34..c424eacd3 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -40,4 +40,4 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** Miscellaneous functions *)
 
-val last_section_hyps : dir_path -> identifier list
+val last_section_hyps : dir_path -> Id.t list
diff --git a/library/global.mli b/library/global.mli
index 82b7cc8eb..fdada3f87 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -35,22 +35,22 @@ val named_context : unit -> Sign.named_context
 val env_is_empty : unit -> bool
 
 (** {6 Extending env with variables and local definitions } *)
-val push_named_assum : (identifier * types) -> Univ.constraints
-val push_named_def   : (identifier * constr * types option) -> Univ.constraints
+val push_named_assum : (Id.t * types) -> Univ.constraints
+val push_named_def   : (Id.t * constr * types option) -> Univ.constraints
 
 (** {6 ... } *)
 (** Adding constants, inductives, modules and module types.  All these
   functions verify that given names match those generated by kernel *)
 
 val add_constant :
-  dir_path -> identifier -> global_declaration -> constant
+  dir_path -> Id.t -> global_declaration -> constant
 val add_mind        :
-  dir_path -> identifier -> mutual_inductive_entry -> mutual_inductive
+  dir_path -> Id.t -> mutual_inductive_entry -> mutual_inductive
 
 val add_module      :
- identifier -> module_entry -> inline -> module_path * delta_resolver
+ Id.t -> module_entry -> inline -> module_path * delta_resolver
 val add_modtype     :
- identifier -> module_struct_entry -> inline -> module_path
+ Id.t -> module_struct_entry -> inline -> module_path
 val add_include :
  module_struct_entry -> bool -> inline -> delta_resolver
 
@@ -65,16 +65,16 @@ val set_engagement : engagement -> unit
 (** [start_*] functions return the [module_path] valid for components
    of the started module / module type *)
 
-val start_module : identifier -> module_path
+val start_module : Id.t -> module_path
 
-val end_module : Summary.frozen ->identifier ->
+val end_module : Summary.frozen ->Id.t ->
   (module_struct_entry * inline) option -> module_path * delta_resolver
 
 val add_module_parameter :
  mod_bound_id -> module_struct_entry -> inline -> delta_resolver
 
-val start_modtype : identifier -> module_path
-val end_modtype : Summary.frozen -> identifier -> module_path
+val start_modtype : Id.t -> module_path
+val end_modtype : Summary.frozen -> Id.t -> module_path
 val pack_module : unit -> module_body
 
 
diff --git a/library/globnames.ml b/library/globnames.ml
index b5312e574..9ce5451a1 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -29,7 +29,7 @@ let eq_gr gr1 gr2 =
     | ConstRef con1, ConstRef con2 -> eq_constant con1 con2
     | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
     | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
-    | VarRef v1, VarRef v2 -> id_eq v1 v2
+    | VarRef v1, VarRef v2 -> Id.equal v1 v2
     | _ -> false
 
 let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef"
@@ -87,7 +87,7 @@ let global_ord_gen fc fmi x y =
     | ConstructRef (indx,jx), ConstructRef (indy,jy) ->
       let c = Int.compare jx jy in
       if Int.equal c 0 then ind_ord indx indy else c
-    | VarRef v1, VarRef v2 -> id_ord v1 v2
+    | VarRef v1, VarRef v2 -> Id.compare v1 v2
     | _, _ -> Pervasives.compare x y
 
 let global_ord_can = global_ord_gen canonical_con canonical_mind
diff --git a/library/globnames.mli b/library/globnames.mli
index af1f10ee4..b82c68ea7 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -80,10 +80,10 @@ val constr_of_global_or_constr : global_reference_or_constr -> constr
 
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
-val encode_mind : dir_path -> identifier -> mutual_inductive
-val decode_mind : mutual_inductive -> dir_path * identifier
-val encode_con : dir_path -> identifier -> constant
-val decode_con : constant -> dir_path * identifier
+val encode_mind : dir_path -> Id.t -> mutual_inductive
+val decode_mind : mutual_inductive -> dir_path * Id.t
+val encode_con : dir_path -> Id.t -> constant
+val decode_con : constant -> dir_path * Id.t
 
 (** {6 Popping one level of section in global names } *)
 
diff --git a/library/goptions.ml b/library/goptions.ml
index 460b153de..858ebbfc8 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -342,7 +342,7 @@ let msg_option_value (name,v) =
     | IntValue (Some n) -> int n
     | IntValue None   -> str "undefined"
     | StringValue s   -> str s
-(*     | IdentValue r    -> pr_global_env Idset.empty r *)
+(*     | IdentValue r    -> pr_global_env Id.Set.empty r *)
 
 let print_option_value key =
   let (name, depr, (_,read,_,_,_)) = get_option key in
diff --git a/library/impargs.ml b/library/impargs.ml
index 8df8420c8..e2abb0925 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -264,7 +264,7 @@ type force_inference = bool (* true = always infer, never turn into evar/subgoal
 
 type implicit_status =
     (* None = Not implicit *)
-    (identifier * implicit_explanation * (maximal_insertion * force_inference)) option
+    (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option
 
 type implicit_side_condition = DefaultImpArgs | LessArgsThan of int
 
@@ -326,7 +326,7 @@ let check_correct_manual_implicits autoimps l =
   List.iter (function
     | ExplByName id,(b,fi,forced) ->
 	if not forced then
-	  error ("Wrong or non-dependent implicit argument name: "^(string_of_id id)^".")
+	  error ("Wrong or non-dependent implicit argument name: "^(Id.to_string id)^".")
     | ExplByPos (i,_id),_t ->
 	if i<1 or i>List.length autoimps then
 	  error ("Bad implicit argument number: "^(string_of_int i)^".")
@@ -340,7 +340,7 @@ let set_manual_implicits env flags enriching autoimps l =
     try
       let (id, (b, fi, fo)), l' = assoc_by_pos k l in
 	if fo then
-	  let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in
+	  let id = match id with Some id -> id | None -> Id.of_string ("arg_" ^ string_of_int k) in
 	    l', Some (id,Manual,(b,fi))
 	else l, None
     with Not_found -> l, None
diff --git a/library/impargs.mli b/library/impargs.mli
index 79d506568..66d72abbb 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -68,7 +68,7 @@ type implicit_explanation =
 type maximal_insertion = bool (** true = maximal contextual insertion *)
 type force_inference = bool (** true = always infer, never turn into evar/subgoal *)
 
-type implicit_status = (identifier * implicit_explanation * 
+type implicit_status = (Id.t * implicit_explanation * 
 			  (maximal_insertion * force_inference)) option
     (** [None] = Not implicit *)
 
@@ -78,7 +78,7 @@ type implicits_list = implicit_side_condition * implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
-val name_of_implicit : implicit_status -> identifier
+val name_of_implicit : implicit_status -> Id.t
 val maximal_insertion_of : implicit_status -> bool
 val force_inference_of : implicit_status -> bool
 
diff --git a/library/lib.ml b/library/lib.ml
index 2653b8418..6e82bfcb6 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -31,7 +31,7 @@ and library_entry = object_name * node
 
 and library_segment = library_entry list
 
-type lib_objects =  (Names.identifier * obj) list
+type lib_objects =  (Names.Id.t * obj) list
 
 let module_kind is_type =
   if is_type then "module type" else "module"
@@ -214,7 +214,7 @@ let add_entry sp node =
 
 let anonymous_id =
   let n = ref 0 in
-  fun () -> incr n; Names.id_of_string ("_" ^ (string_of_int !n))
+  fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n))
 
 let add_anonymous_entry node =
   let id = anonymous_id () in
@@ -387,8 +387,8 @@ let find_opening_node id =
   try
     let oname,entry = find_entry_p is_opening_node in
     let id' = basename (fst oname) in
-    if not (Names.id_eq id id') then
-      error ("Last block to end has name "^(Names.string_of_id id')^".");
+    if not (Names.Id.equal id id') then
+      error ("Last block to end has name "^(Names.Id.to_string id')^".");
     entry
   with Not_found -> error "There is nothing to end."
 
@@ -401,12 +401,12 @@ let find_opening_node id =
    - the list of substitution to do at section closing
 *)
 
-type variable_info = Names.identifier * Decl_kinds.binding_kind * Term.constr option * Term.types
+type variable_info = Names.Id.t * Decl_kinds.binding_kind * Term.constr option * Term.types
 type variable_context = variable_info list
 type abstr_list = variable_context Names.Cmap.t * variable_context Names.Mindmap.t
 
 let sectab =
-  ref ([] : ((Names.identifier * Decl_kinds.binding_kind) list *
+  ref ([] : ((Names.Id.t * Decl_kinds.binding_kind) list *
 		Cooking.work_list * abstr_list) list)
 
 let add_section () =
@@ -420,7 +420,7 @@ let add_section_variable id impl =
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | ((id,impl)::idl,(id',b,t)::hyps) when Names.id_eq id id' ->
+    | ((id,impl)::idl,(id',b,t)::hyps) when Names.Id.equal id id' ->
       (id',impl,b,t) :: aux (idl,hyps)
     | (id::idl,hyps) -> aux (idl,hyps)
     | [], _ -> []
@@ -461,7 +461,7 @@ let section_segment_of_mutual_inductive kn =
 
 let rec list_mem_assoc x = function
   | [] -> raise Not_found
-  | (a, _) :: l -> Int.equal (Names.id_ord a x) 0 || list_mem_assoc x l
+  | (a, _) :: l -> Int.equal (Names.Id.compare a x) 0 || list_mem_assoc x l
 
 let section_instance = function
   | VarRef id ->
@@ -612,7 +612,7 @@ let label_before_name (loc,id) =
     | (_, Leaf o) when !found && String.equal (object_tag o) "DOT" -> true
     | ((fp, _),_) ->
       let (_, name) = repr_path fp in
-      let () = if Names.id_eq id name then found := true in
+      let () = if Names.Id.equal id name then found := true in
       false
   in
   match find_entry_p search with
@@ -657,7 +657,7 @@ let rec split_mp mp =
     | Names.MPfile dp -> dp,  Names.empty_dirpath
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
-	  mprec, Names.make_dirpath (Names.id_of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
+	  mprec, Names.make_dirpath (Names.Id.of_string (Names.string_of_label lbl) :: (Names.repr_dirpath dprec))
     | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.make_dirpath [id]
 
 let split_modpath mp =
diff --git a/library/lib.mli b/library/lib.mli
index 25c0e1b24..75e18b194 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -27,7 +27,7 @@ type node =
 
 and library_segment = (Libnames.object_name * node) list
 
-type lib_objects = (Names.identifier * Libobject.obj) list
+type lib_objects = (Names.Id.t * Libobject.obj) list
 
 (** {6 Object iteration functions. } *)
 
@@ -53,12 +53,12 @@ val segment_of_objects :
 (** Adding operations (which call the [cache] method, and getting the
   current list of operations (most recent ones coming first). *)
 
-val add_leaf : Names.identifier -> Libobject.obj -> Libnames.object_name
+val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name
 val add_anonymous_leaf : Libobject.obj -> unit
 
 (** this operation adds all objects with the same name and calls [load_object]
    for each of them *)
-val add_leaves : Names.identifier -> Libobject.obj list -> Libnames.object_name
+val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name
 
 val add_frozen_state : unit -> unit
 
@@ -75,14 +75,14 @@ val contents_after : Libnames.object_name option -> library_segment
 val cwd : unit -> Names.dir_path
 val cwd_except_section : unit -> Names.dir_path
 val current_dirpath : bool -> Names.dir_path (* false = except sections *)
-val make_path : Names.identifier -> Libnames.full_path
-val make_path_except_section : Names.identifier -> Libnames.full_path
+val make_path : Names.Id.t -> Libnames.full_path
+val make_path_except_section : Names.Id.t -> Libnames.full_path
 val path_of_include : unit -> Libnames.full_path
 
 (** Kernel-side names *)
 val current_prefix : unit -> Names.module_path * Names.dir_path
-val make_kn : Names.identifier -> Names.kernel_name
-val make_con : Names.identifier -> Names.constant
+val make_kn : Names.Id.t -> Names.kernel_name
+val make_con : Names.Id.t -> Names.constant
 
 (** Are we inside an opened section *)
 val sections_are_opened : unit -> bool
@@ -98,7 +98,7 @@ val is_module : unit -> bool
 val current_mod_id : unit -> Names.module_ident
 
 (** Returns the opening node of a given name *)
-val find_opening_node : Names.identifier -> node
+val find_opening_node : Names.Id.t -> node
 
 (** {6 Modules and module types } *)
 
@@ -134,13 +134,13 @@ val library_dp : unit -> Names.dir_path
 (** Extract the library part of a name even if in a section *)
 val dp_of_mp : Names.module_path -> Names.dir_path
 val split_mp : Names.module_path -> Names.dir_path * Names.dir_path
-val split_modpath : Names.module_path -> Names.dir_path * Names.identifier list
+val split_modpath : Names.module_path -> Names.dir_path * Names.Id.t list
 val library_part :  Globnames.global_reference -> Names.dir_path
 val remove_section_part : Globnames.global_reference -> Names.dir_path
 
 (** {6 Sections } *)
 
-val open_section : Names.identifier -> unit
+val open_section : Names.Id.t -> unit
 val close_section : unit -> unit
 
 (** {6 Backtracking } *)
@@ -164,7 +164,7 @@ val first_command_label : int
 val reset_label : int -> unit
 
 (** search the label registered immediately before adding some definition *)
-val label_before_name : Names.identifier Loc.located -> int
+val label_before_name : Names.Id.t Loc.located -> int
 
 (** {6 We can get and set the state of the operations (used in [States]). } *)
 
@@ -176,29 +176,29 @@ val unfreeze : frozen -> unit
 val init : unit -> unit
 
 (** XML output hooks *)
-val set_xml_open_section : (Names.identifier -> unit) -> unit
-val set_xml_close_section : (Names.identifier -> unit) -> unit
+val set_xml_open_section : (Names.Id.t -> unit) -> unit
+val set_xml_close_section : (Names.Id.t -> unit) -> unit
 
 (** {6 Section management for discharge } *)
-type variable_info = Names.identifier * Decl_kinds.binding_kind *
+type variable_info = Names.Id.t * Decl_kinds.binding_kind *
     Term.constr option * Term.types
 type variable_context = variable_info list
 
-val instance_from_variable_context : variable_context -> Names.identifier array
+val instance_from_variable_context : variable_context -> Names.Id.t array
 val named_of_variable_context : variable_context -> Sign.named_context
 
 val section_segment_of_constant : Names.constant -> variable_context
 val section_segment_of_mutual_inductive: Names.mutual_inductive -> variable_context
 
-val section_instance : Globnames.global_reference -> Names.identifier array
+val section_instance : Globnames.global_reference -> Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
-val add_section_variable : Names.identifier -> Decl_kinds.binding_kind -> unit
+val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> unit
 
 val add_section_constant : Names.constant -> Sign.named_context -> unit
 val add_section_kn : Names.mutual_inductive -> Sign.named_context -> unit
 val replacement_context : unit ->
-  (Names.identifier array Names.Cmap.t * Names.identifier array Names.Mindmap.t)
+  (Names.Id.t array Names.Cmap.t * Names.Id.t array Names.Mindmap.t)
 
 (** {6 Discharge: decrease the section level if in the current section } *)
 
diff --git a/library/libnames.ml b/library/libnames.ml
index a0eff296c..ee24b2575 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -59,7 +59,7 @@ let parse_dir s =
     in
     if Int.equal pos n then error (s ^ " is an invalid path.");
     let dir = String.sub s n (pos-n) in
-    decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
+    decoupe_dirs ((Id.of_string dir)::dirs) (pos+1)
   in
     decoupe_dirs [] 0
 
@@ -80,10 +80,10 @@ module Dirmap = Map.Make(struct type t = dir_path let compare = dir_path_ord end
 
 type full_path = {
   dirpath : dir_path ;
-  basename : identifier }
+  basename : Id.t }
 
 let eq_full_path p1 p2 =
-  id_eq p1.basename p2.basename &&
+  Id.equal p1.basename p2.basename &&
   Int.equal (dir_path_ord p1.dirpath p2.dirpath) 0
 
 let make_path pa id = { dirpath = pa; basename = id }
@@ -94,14 +94,14 @@ let repr_path { dirpath = pa; basename = id } = (pa,id)
 let string_of_path sp =
   let (sl,id) = repr_path sp in
   match repr_dirpath sl with
-  | [] -> string_of_id id
-  | _ -> (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+  | [] -> Id.to_string id
+  | _ -> (string_of_dirpath sl) ^ "." ^ (Id.to_string id)
 
 let sp_ord sp1 sp2 =
   let (p1,id1) = repr_path sp1
   and (p2,id2) = repr_path sp2 in
   let p_bit = compare p1 p2 in
-  if Int.equal p_bit 0 then id_ord id1 id2 else p_bit
+  if Int.equal p_bit 0 then Id.compare id1 id2 else p_bit
 
 module SpOrdered =
   struct
@@ -178,7 +178,7 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with
 
 type reference =
   | Qualid of qualid Loc.located
-  | Ident of identifier Loc.located
+  | Ident of Id.t Loc.located
 
 let qualid_of_reference = function
   | Qualid (loc,qid) -> loc, qid
@@ -186,11 +186,11 @@ let qualid_of_reference = function
 
 let string_of_reference = function
   | Qualid (loc,qid) -> string_of_qualid qid
-  | Ident (loc,id) -> string_of_id id
+  | Ident (loc,id) -> Id.to_string id
 
 let pr_reference = function
   | Qualid (_,qid) -> pr_qualid qid
-  | Ident (_,id) -> str (string_of_id id)
+  | Ident (_,id) -> str (Id.to_string id)
 
 let loc_of_reference = function
   | Qualid (loc,qid) -> loc
@@ -198,7 +198,7 @@ let loc_of_reference = function
 
 let eq_reference r1 r2 = match r1, r2 with
 | Qualid (_, q1), Qualid (_, q2) -> qualid_eq q1 q2
-| Ident (_, id1), Ident (_, id2) -> id_eq id1 id2
+| Ident (_, id1), Ident (_, id2) -> Id.equal id1 id2
 | _ -> false
 
 (* Deprecated synonyms *)
diff --git a/library/libnames.mli b/library/libnames.mli
index 434041f77..08330349e 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -23,7 +23,7 @@ val pop_dirpath : dir_path -> dir_path
 val pop_dirpath_n : int -> dir_path -> dir_path
 
 (** Give the immediate prefix and basename of a [dir_path] *)
-val split_dirpath : dir_path -> dir_path * identifier
+val split_dirpath : dir_path -> dir_path * Id.t
 
 val add_dirpath_suffix : dir_path -> module_ident -> dir_path
 val add_dirpath_prefix : module_ident -> dir_path -> dir_path
@@ -43,12 +43,12 @@ type full_path
 val eq_full_path : full_path -> full_path -> bool
 
 (** Constructors of [full_path] *)
-val make_path : dir_path -> identifier -> full_path
+val make_path : dir_path -> Id.t -> full_path
 
 (** Destructors of [full_path] *)
-val repr_path : full_path -> dir_path * identifier
+val repr_path : full_path -> dir_path * Id.t
 val dirpath : full_path -> dir_path
-val basename : full_path -> identifier
+val basename : full_path -> Id.t
 
 (** Parsing and printing of section path as ["coq_root.module.id"] *)
 val path_of_string : string -> full_path
@@ -67,8 +67,8 @@ val restrict_path : int -> full_path -> full_path
 
 type qualid
 
-val make_qualid : dir_path -> identifier -> qualid
-val repr_qualid : qualid -> dir_path * identifier
+val make_qualid : dir_path -> Id.t -> qualid
+val repr_qualid : qualid -> dir_path * Id.t
 
 val qualid_eq : qualid -> qualid -> bool
 
@@ -76,12 +76,12 @@ val pr_qualid : qualid -> std_ppcmds
 val string_of_qualid : qualid -> string
 val qualid_of_string : string -> qualid
 
-(** Turns an absolute name, a dirpath, or an identifier into a
+(** Turns an absolute name, a dirpath, or an Id.t into a
    qualified name denoting the same name *)
 
 val qualid_of_path : full_path -> qualid
 val qualid_of_dirpath : dir_path -> qualid
-val qualid_of_ident : identifier -> qualid
+val qualid_of_ident : Id.t -> qualid
 
 (** Both names are passed to objects: a "semantic" [kernel_name], which
    can be substituted and a "syntactic" [full_path] which can be printed
@@ -93,7 +93,7 @@ type object_prefix = dir_path * (module_path * dir_path)
 
 val eq_op : object_prefix -> object_prefix -> bool
 
-val make_oname : object_prefix -> identifier -> object_name
+val make_oname : object_prefix -> Id.t -> object_name
 
 (** to this type are mapped [dir_path]'s in the nametab *)
 type global_dir_reference =
@@ -114,7 +114,7 @@ val eq_global_dir_reference :
 
 type reference =
   | Qualid of qualid located
-  | Ident of identifier located
+  | Ident of Id.t located
 
 val eq_reference : reference -> reference -> bool
 val qualid_of_reference : reference -> qualid located
@@ -124,5 +124,5 @@ val loc_of_reference : reference -> Loc.t
 
 (** Deprecated synonyms *)
 
-val make_short_qualid : identifier -> qualid (** = qualid_of_ident *)
+val make_short_qualid : Id.t -> qualid (** = qualid_of_ident *)
 val qualid_of_sp : full_path -> qualid (** = qualid_of_path *)
diff --git a/library/library.ml b/library/library.ml
index ec84a75e8..b25b1d313 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) =
 
 let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
-    (List.map string_of_id (List.rev (repr_dirpath dir)))
+    (List.map Id.to_string (List.rev (repr_dirpath dir)))
 
 let root_paths_matching_dir_path dir =
   let rec aux = function
@@ -330,7 +330,7 @@ let locate_absolute_library dir =
   let loadpath = root_paths_matching_dir_path pref in
   let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
   try
-    let name = (string_of_id base)^".vo" in
+    let name = (Id.to_string base)^".vo" in
     let _, file = System.where_in_path ~warn:false loadpath name in
     (dir, file)
   with Not_found ->
@@ -346,7 +346,7 @@ let locate_qualified_library warn qid =
     let dir, base = repr_qualid qid in
     let loadpath = loadpaths_matching_dir_path dir in
     let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in
-    let name = string_of_id base ^ ".vo" in
+    let name = Id.to_string base ^ ".vo" in
     let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in
     let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in
     (* Look if loaded *)
@@ -450,7 +450,7 @@ let rec_intern_library needed mref =
   let _,needed = intern_library needed mref in needed
 
 let check_library_short_name f dir = function
-  | Some id when not (id_eq id (snd (split_dirpath dir))) ->
+  | Some id when not (Id.equal id (snd (split_dirpath dir))) ->
       errorlabstrm "check_library_short_name"
       (str ("The file " ^ f ^ " contains library") ++ spc () ++
       pr_dirpath dir ++ spc () ++ str "and not library" ++ spc () ++
@@ -598,9 +598,9 @@ let import_module export (loc,qid) =
 let check_coq_overwriting p id =
   let l = repr_dirpath p in
   let is_empty = match l with [] -> true | _ -> false in
-  if not !Flags.boot && not is_empty && String.equal (string_of_id (List.last l)) "Coq" then
+  if not !Flags.boot && not is_empty && String.equal (Id.to_string (List.last l)) "Coq" then
     errorlabstrm ""
-      (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^
+      (strbrk ("Cannot build module "^string_of_dirpath p^"."^Id.to_string id^
       ": it starts with prefix \"Coq\" which is reserved for the Coq library."))
 
 let start_library f =
@@ -608,7 +608,7 @@ let start_library f =
   let _,longf =
     System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
-  let id = id_of_string (Filename.basename f) in
+  let id = Id.of_string (Filename.basename f) in
   check_coq_overwriting ldir0 id;
   let ldir = add_dirpath_suffix ldir0 id in
   Declaremods.start_library ldir;
diff --git a/library/library.mli b/library/library.mli
index f17ea8b6e..4e88a85b5 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -26,7 +26,7 @@ open Libobject
 val require_library : qualid located list -> bool option -> unit
 val require_library_from_dirpath : (dir_path * string) list -> bool option -> unit
 val require_library_from_file :
-  identifier option -> CUnix.physical_path -> bool option -> unit
+  Id.t option -> CUnix.physical_path -> bool option -> unit
 
 (** {6 ... } *)
 (** Open a module (or a library); if the boolean is true then it's also
diff --git a/library/nameops.ml b/library/nameops.ml
index 461e7a405..f8f95135f 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -12,7 +12,7 @@ open Names
 
 (* Identifiers *)
 
-let pr_id id = str (string_of_id id)
+let pr_id id = str (Id.to_string id)
 
 let pr_name = function
   | Anonymous -> str "_"
@@ -24,7 +24,7 @@ let code_of_0 = Char.code '0'
 let code_of_9 = Char.code '9'
 
 let cut_ident skip_quote s =
-  let s = string_of_id s in
+  let s = Id.to_string s in
   let slen = String.length s in
   (* [n'] is the position of the first non nullary digit *)
   let rec numpart n n' =
@@ -46,7 +46,7 @@ let cut_ident skip_quote s =
 
 let repr_ident s =
   let numstart = cut_ident false s in
-  let s = string_of_id s in
+  let s = Id.to_string s in
   let slen = String.length s in
   if Int.equal numstart slen then
     (s, None)
@@ -60,17 +60,17 @@ let make_ident sa = function
       let s =
         if c < code_of_0 or c > code_of_9 then sa ^ (string_of_int n)
         else sa ^ "_" ^ (string_of_int n) in
-      id_of_string s
-  | None -> id_of_string (String.copy sa)
+      Id.of_string s
+  | None -> Id.of_string (String.copy sa)
 
 let root_of_id id =
   let suffixstart = cut_ident true id in
-  id_of_string (String.sub (string_of_id id) 0 suffixstart)
+  Id.of_string (String.sub (Id.to_string id) 0 suffixstart)
 
 (* Rem: semantics is a bit different, if an ident starts with toto00 then
   after successive renamings it comes to toto09, then it goes on with toto10 *)
 let lift_subscript id =
-  let id = string_of_id id in
+  let id = Id.to_string id in
   let len = String.length id in
   let rec add carrypos =
     let c = id.[carrypos] in
@@ -93,20 +93,20 @@ let lift_subscript id =
       end;
       newid
     end
-  in id_of_string (add (len-1))
+  in Id.of_string (add (len-1))
 
 let has_subscript id =
-  let id = string_of_id id in
+  let id = Id.to_string id in
   is_digit (id.[String.length id - 1])
 
 let forget_subscript id =
   let numstart = cut_ident false id in
   let newid = String.make (numstart+1) '0' in
-  String.blit (string_of_id id) 0 newid 0 numstart;
-  (id_of_string newid)
+  String.blit (Id.to_string id) 0 newid 0 numstart;
+  (Id.of_string newid)
 
-let add_suffix id s = id_of_string (string_of_id id ^ s)
-let add_prefix s id = id_of_string (s ^ string_of_id id)
+let add_suffix id s = Id.of_string (Id.to_string id ^ s)
+let add_prefix s id = Id.of_string (s ^ Id.to_string id)
 
 let atompart_of_id id = fst (repr_ident id)
 
@@ -141,7 +141,7 @@ let pr_lab l = str (string_of_label l)
 let default_library = Names.initial_dir (* = ["Top"] *)
 
 (*s Roots of the space of absolute names *)
-let coq_root = id_of_string "Coq"
+let coq_root = Id.of_string "Coq"
 let default_root_prefix = make_dirpath []
 
 (* Metavariables *)
diff --git a/library/nameops.mli b/library/nameops.mli
index fb26c1910..3bdd64f75 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -9,31 +9,31 @@
 open Names
 
 (** Identifiers and names *)
-val pr_id : identifier -> Pp.std_ppcmds
+val pr_id : Id.t -> Pp.std_ppcmds
 val pr_name : name -> Pp.std_ppcmds
 
-val make_ident : string -> int option -> identifier
-val repr_ident : identifier -> string * int option
+val make_ident : string -> int option -> Id.t
+val repr_ident : Id.t -> string * int option
 
-val atompart_of_id : identifier -> string  (** remove trailing digits *)
-val root_of_id : identifier -> identifier (** remove trailing digits, ' and _ *)
+val atompart_of_id : Id.t -> string  (** remove trailing digits *)
+val root_of_id : Id.t -> Id.t (** remove trailing digits, ' and _ *)
 
-val add_suffix : identifier -> string -> identifier
-val add_prefix : string -> identifier -> identifier
+val add_suffix : Id.t -> string -> Id.t
+val add_prefix : string -> Id.t -> Id.t
 
-val has_subscript    : identifier -> bool
-val lift_subscript   : identifier -> identifier
-val forget_subscript : identifier -> identifier
+val has_subscript    : Id.t -> bool
+val lift_subscript   : Id.t -> Id.t
+val forget_subscript : Id.t -> Id.t
 
-val out_name : name -> identifier
+val out_name : name -> Id.t
 (** [out_name] associates [id] to [Name id]. Raises [Failure "Nameops.out_name"]
     otherwise. *)
 
-val name_fold : (identifier -> 'a -> 'a) -> name -> 'a -> 'a
-val name_iter : (identifier -> unit) -> name -> unit
-val name_cons : name -> identifier list -> identifier list
-val name_app : (identifier -> identifier) -> name -> name
-val name_fold_map : ('a -> identifier -> 'a * identifier) -> 'a -> name -> 'a * name
+val name_fold : (Id.t -> 'a -> 'a) -> name -> 'a -> 'a
+val name_iter : (Id.t -> unit) -> name -> unit
+val name_cons : name -> Id.t list -> Id.t list
+val name_app : (Id.t -> Id.t) -> name -> name
+val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> name -> 'a * name
 
 
 val pr_lab : label -> Pp.std_ppcmds
diff --git a/library/nametab.ml b/library/nametab.ml
index 7c1100165..bbcee8b66 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -48,7 +48,7 @@ module type UserName = sig
   type t
   val equal : t -> t -> bool
   val to_string : t -> string
-  val repr : t -> identifier * module_ident list
+  val repr : t -> Id.t * module_ident list
 end
 
 module type EqualityType =
@@ -77,7 +77,7 @@ module type NAMETREE = sig
   val find : user_name -> t -> elt
   val exists : user_name -> t -> bool
   val user_name : qualid -> t -> user_name
-  val shortest_qualid : Idset.t -> user_name -> t -> qualid
+  val shortest_qualid : Id.Set.t -> user_name -> t -> qualid
   val find_prefixes : qualid -> t -> elt list
 end
 
@@ -101,9 +101,9 @@ struct
   let mktree p m = { path=p; map=m }
   let empty_tree = mktree Nothing ModIdmap.empty
 
-  type t = nametree Idmap.t
+  type t = nametree Id.Map.t
 
-  let empty = Idmap.empty
+  let empty = Id.Map.empty
 
   (* [push_until] is used to register [Until vis] visibility and
      [push_exactly] to [Exactly vis] and [push_tree] chooses the right one*)
@@ -178,14 +178,14 @@ let rec push_exactly uname o level tree = function
 let push visibility uname o tab =
   let id,dir = U.repr uname in
   let ptab =
-    try Idmap.find id tab
+    try Id.Map.find id tab
     with Not_found -> empty_tree
   in
   let ptab' = match visibility with
     | Until i -> push_until uname o (i-1) ptab dir
     | Exactly i -> push_exactly uname o (i-1) ptab dir
   in
-    Idmap.add id ptab' tab
+    Id.Map.add id ptab' tab
 
 
 let rec search tree = function
@@ -194,7 +194,7 @@ let rec search tree = function
 
 let find_node qid tab =
   let (dir,id) = repr_qualid qid in
-    search (Idmap.find id tab) (repr_dirpath dir)
+    search (Id.Map.find id tab) (repr_dirpath dir)
 
 let locate qid tab =
   let o = match find_node qid tab with
@@ -212,7 +212,7 @@ let user_name qid tab =
 
 let find uname tab =
   let id,l = U.repr uname in
-    match search (Idmap.find id tab) l with
+    match search (Id.Map.find id tab) l with
 	Absolute (_,o) -> o
       | _ -> raise Not_found
 
@@ -225,7 +225,7 @@ let exists uname tab =
 
 let shortest_qualid ctx uname tab =
   let id,dir = U.repr uname in
-  let hidden = Idset.mem id ctx in
+  let hidden = Id.Set.mem id ctx in
   let rec find_uname pos dir tree =
     let is_empty = match pos with [] -> true | _ -> false in
     match tree.path with
@@ -236,7 +236,7 @@ let shortest_qualid ctx uname tab =
 	    [] -> raise Not_found
 	  | id::dir -> find_uname (id::pos) dir (ModIdmap.find id tree.map)
   in
-  let ptab = Idmap.find id tab in
+  let ptab = Id.Map.find id tab in
   let found_dir = find_uname [] dir ptab in
     make_qualid (make_dirpath found_dir) id
 
@@ -256,7 +256,7 @@ let rec search_prefixes tree = function
 let find_prefixes qid tab =
   try
     let (dir,id) = repr_qualid qid in
-    search_prefixes (Idmap.find id tab) (repr_dirpath dir)
+    search_prefixes (Id.Map.find id tab) (repr_dirpath dir)
   with Not_found -> []
 
 end
@@ -520,15 +520,15 @@ let shortest_qualid_of_syndef ctx kn =
 
 let shortest_qualid_of_module mp =
   let dir = MPmap.find mp !the_modrevtab in
-    DirTab.shortest_qualid Idset.empty dir !the_dirtab
+    DirTab.shortest_qualid Id.Set.empty dir !the_dirtab
 
 let shortest_qualid_of_modtype kn =
   let sp = MPmap.find kn !the_modtyperevtab in
-    MPTab.shortest_qualid Idset.empty sp !the_modtypetab
+    MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab
 
 let shortest_qualid_of_tactic kn =
   let sp = KNmap.find kn !the_tacticrevtab in
-    KnTab.shortest_qualid Idset.empty sp !the_tactictab
+    KnTab.shortest_qualid Id.Set.empty sp !the_tactictab
 
 let pr_global_env env ref =
   (* Il est important de laisser le let-in, car les streams s'évaluent
diff --git a/library/nametab.mli b/library/nametab.mli
index 8c22749b5..8a18166a9 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -51,7 +51,7 @@ open Globnames
    {- [shortest_qualid_of : object_reference -> user_name]
 
      The [user_name] can be for example the shortest non ambiguous [qualid] or
-     the [full_user_name] or [identifier]. Such a function can also have a
+     the [full_user_name] or [Id.t]. Such a function can also have a
      local context argument.}}
 
 *)
@@ -149,18 +149,18 @@ val path_of_tactic : ltac_constant -> full_path
    associated to global reference *)
 
 val dirpath_of_global : global_reference -> dir_path
-val basename_of_global : global_reference -> identifier
+val basename_of_global : global_reference -> Id.t
 
 (** Printing of global references using names as short as possible *)
-val pr_global_env : Idset.t -> global_reference -> std_ppcmds
+val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds
 
 
 (** The [shortest_qualid] functions given an object with [user_name]
    Coq.A.B.x, try to find the shortest among x, B.x, A.B.x and
    Coq.A.B.x that denotes the same object. *)
 
-val shortest_qualid_of_global : Idset.t -> global_reference -> qualid
-val shortest_qualid_of_syndef : Idset.t -> syndef_name -> qualid
+val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid
+val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid
 val shortest_qualid_of_modtype : module_path -> qualid
 val shortest_qualid_of_module : module_path -> qualid
 val shortest_qualid_of_tactic : ltac_constant -> qualid