Modulification of identifier

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

36 files changed, 289 insertions, 204 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 994242a8a..382fcf7f2 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -121,7 +121,7 @@ type instruction =
 
 and bytecodes = instruction list
 
-type fv_elem = FVnamed of identifier | FVrel of int
+type fv_elem = FVnamed of Id.t | FVrel of int
 
 type fv = fv_elem array
 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 0a631987e..0698f3836 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -114,7 +114,7 @@ type instruction =
 
 and bytecodes = instruction list
 
-type fv_elem = FVnamed of identifier | FVrel of int
+type fv_elem = FVnamed of Id.t | FVrel of int
 
 type fv = fv_elem array
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 1d2587efe..021e50847 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -188,7 +188,7 @@ let find_at f l =
 let pos_named id r =
   let env = !(r.in_env) in
   let cid = FVnamed id in
-  let f = function FVnamed id' -> id_eq id id' | _ -> false in
+  let f = function FVnamed id' -> Id.equal id id' | _ -> false in
   try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
   with Not_found ->
     let pos = env.size in
@@ -710,7 +710,7 @@ let compile env c =
   Format.print_string "fv = ";
   List.iter (fun v ->
     match v with
-    | FVnamed id -> Format.print_string ((string_of_id id)^"; ")
+    | FVnamed id -> Format.print_string ((Id.to_string id)^"; ")
     | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv;  Format
     .print_string "\n";
   Format.print_flush();  *)
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 370053275..934701f43 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -65,10 +65,10 @@ let with_stats c =
   end else
     Lazy.force c
 
-let all_opaque = (Idpred.empty, Cpred.empty)
-let all_transparent = (Idpred.full, Cpred.full)
+let all_opaque = (Id.Pred.empty, Cpred.empty)
+let all_transparent = (Id.Pred.full, Cpred.full)
 
-let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
 let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
 
 module type RedFlagsSig = sig
@@ -80,7 +80,7 @@ module type RedFlagsSig = sig
   val fIOTA : red_kind
   val fZETA : red_kind
   val fCONST : constant -> red_kind
-  val fVAR : identifier -> red_kind
+  val fVAR : Id.t -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
   val red_sub : reds -> red_kind -> reds
@@ -104,7 +104,7 @@ module RedFlags = (struct
     r_iota : bool }
 
   type red_kind = BETA | DELTA | ETA | IOTA | ZETA
-	      | CONST of constant | VAR of identifier
+	      | CONST of constant | VAR of Id.t
   let fBETA = BETA
   let fDELTA = DELTA
   let fETA = ETA
@@ -131,7 +131,7 @@ module RedFlags = (struct
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
 	let (l1,l2) = red.r_const in
-	{ red with r_const = Idpred.add id l1, l2 }
+	{ red with r_const = Id.Pred.add id l1, l2 }
 
   let red_sub red = function
     | BETA -> { red with r_beta = false }
@@ -144,7 +144,7 @@ module RedFlags = (struct
     | ZETA -> { red with r_zeta = false }
     | VAR id ->
 	let (l1,l2) = red.r_const in
-	{ red with r_const = Idpred.remove id l1, l2 }
+	{ red with r_const = Id.Pred.remove id l1, l2 }
 
   let red_add_transparent red tr =
     { red with r_const = tr }
@@ -160,7 +160,7 @@ module RedFlags = (struct
 	incr_cnt c delta
     | VAR id -> (* En attendant d'avoir des kn pour les Var *)
 	let (l,_) = red.r_const in
-	let c = Idpred.mem id l in
+	let c = Id.Pred.mem id l in
 	incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
     | IOTA -> incr_cnt red.r_iota iota
@@ -225,7 +225,7 @@ type 'a infos = {
   i_env : env;
   i_sigma : existential -> constr option;
   i_rels : constr option array;
-  i_vars : (identifier * constr) list;
+  i_vars : (Id.t * constr) list;
   i_tab : 'a KeyTable.t }
 
 let info_flags info = info.i_flags
@@ -659,7 +659,7 @@ let rec to_constr constr_fun lfts v =
         let fr = mk_clos2 env t in
         let unfv = update v (fr.norm,fr.term) in
         to_constr constr_fun lfts unfv
-    | FLOCKED -> assert false (*mkVar(id_of_string"_LOCK_")*)
+    | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
 
 (* This function defines the correspondance between constr and
    fconstr. When we find a closure whose substitution is the identity,
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 62ebfe3ea..d7a775fde 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -46,7 +46,7 @@ module type RedFlagsSig = sig
   val fIOTA : red_kind
   val fZETA : red_kind
   val fCONST : constant -> red_kind
-  val fVAR : identifier -> red_kind
+  val fVAR : Id.t -> red_kind
 
   (** No reduction at all *)
   val no_red : reds
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 7da2a7faa..6f013e46f 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -23,14 +23,14 @@ let is_transparent = function
 | Level 0 -> true
 | _ -> false
 
-type oracle = level Idmap.t * level Cmap.t
+type oracle = level Id.Map.t * level Cmap.t
 
-let var_opacity = ref Idmap.empty
+let var_opacity = ref Id.Map.empty
 let cst_opacity = ref Cmap.empty
 
 let get_strategy = function
   | VarKey id ->
-      (try Idmap.find id !var_opacity
+      (try Id.Map.find id !var_opacity
       with Not_found -> default)
   | ConstKey c ->
       (try Cmap.find c !cst_opacity
@@ -41,8 +41,8 @@ let set_strategy k l =
   match k with
   | VarKey id ->
       var_opacity :=
-      if l=default then Idmap.remove id !var_opacity
-      else Idmap.add id l !var_opacity
+      if l=default then Id.Map.remove id !var_opacity
+      else Id.Map.add id l !var_opacity
   | ConstKey c ->
       cst_opacity :=
       if l=default then Cmap.remove c !cst_opacity
@@ -50,9 +50,9 @@ let set_strategy k l =
   | RelKey _ -> Errors.error "set_strategy: RelKey"
 
 let get_transp_state () =
-  (Idmap.fold
-    (fun id l ts -> if  l=Opaque then Idpred.remove id ts else ts)
-    !var_opacity Idpred.full,
+  (Id.Map.fold
+    (fun id l ts -> if  l=Opaque then Id.Pred.remove id ts else ts)
+    !var_opacity Id.Pred.full,
    Cmap.fold
     (fun c l ts -> if  l=Opaque then Cpred.remove c ts else ts)
     !cst_opacity Cpred.full)
@@ -67,6 +67,6 @@ let oracle_order l2r k1 k2 =
     | _ -> l2r (* use recommended default *)
 
 (* summary operations *)
-let init() = (cst_opacity := Cmap.empty; var_opacity := Idmap.empty)
+let init() = (cst_opacity := Cmap.empty; var_opacity := Id.Map.empty)
 let freeze () = (!var_opacity, !cst_opacity)
 let unfreeze (vo,co) = (cst_opacity := co; var_opacity := vo)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 99b582fe3..864d2f45a 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -23,7 +23,7 @@ open Environ
 
 (*s Cooking the constants. *)
 
-type work_list = identifier array Cmap.t * identifier array Mindmap.t
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
 
 let pop_dirpath p = match repr_dirpath p with
   | [] -> anomaly "dirpath_prefix: empty dirpath"
@@ -139,7 +139,7 @@ let cook_constant env r =
   in
   let const_hyps =
     Sign.fold_named_context (fun (h,_,_) hyps ->
-      List.filter (fun (id,_,_) -> not (id_eq id h)) hyps)
+      List.filter (fun (id,_,_) -> not (Id.equal id h)) hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
     | NonPolymorphicType t ->
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 1586adae7..7adb00da6 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -14,7 +14,7 @@ open Univ
 
 (** {6 Cooking the constants. } *)
 
-type work_list = identifier array Cmap.t * identifier array Mindmap.t
+type work_list = Id.t array Cmap.t * Id.t array Mindmap.t
 
 type recipe = {
   d_from : constant_body;
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index f44e85320..789df8b3d 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -117,7 +117,7 @@ and slot_for_fv env fv =
 	    let (_, b, _) = Sign.lookup_named id env.env_named_context in
 	    let v,d =
 	      match b with
-		| None -> (val_of_named id, Idset.empty)
+		| None -> (val_of_named id, Id.Set.empty)
 		| Some c -> (val_of_constr env c, Environ.global_vars_set (Environ.env_of_pre_env env) c)
 	    in
 	      nv := VKvalue (v,d); v
@@ -131,7 +131,7 @@ and slot_for_fv env fv =
 	    let (_, b, _) = lookup_rel i env.env_rel_context in
 	    let (v, d) =
 	      match b with
-		| None -> (val_of_rel (nb_rel env - i), Idset.empty)
+		| None -> (val_of_rel (nb_rel env - i), Id.Set.empty)
 		| Some c -> let renv =  env_of_rel i env in
 			      (val_of_constr renv c, Environ.global_vars_set (Environ.env_of_pre_env renv) c)
 	    in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 3e5b10f3b..baeab9142 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -241,7 +241,7 @@ type one_inductive_body = {
 (* Primitive datas *)
 
  (* Name of the type: [Ii] *)
-    mind_typename : identifier;
+    mind_typename : Id.t;
 
  (* Arity context of [Ii] with parameters: [forall params, Ui] *)
     mind_arity_ctxt : rel_context;
@@ -250,7 +250,7 @@ type one_inductive_body = {
     mind_arity : inductive_arity;
 
  (* Names of the constructors: [cij] *)
-    mind_consnames : identifier array;
+    mind_consnames : Id.t array;
 
  (* Types of the constructors with parameters: [forall params, Tij],
     where the Ik are replaced by de Bruijn index in the context
@@ -363,10 +363,10 @@ let hcons_indarity = function
 
 let hcons_mind_packet oib =
  { oib with
-   mind_typename = hcons_ident oib.mind_typename;
+   mind_typename = Id.hcons oib.mind_typename;
    mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt;
    mind_arity = hcons_indarity oib.mind_arity;
-   mind_consnames = Array.smartmap hcons_ident oib.mind_consnames;
+   mind_consnames = Array.smartmap Id.hcons oib.mind_consnames;
    mind_user_lc = Array.smartmap hcons_types oib.mind_user_lc;
    mind_nf_lc = Array.smartmap hcons_types oib.mind_nf_lc }
 
@@ -395,8 +395,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path
-  | With_definition_body of  identifier list * constant_body
+    With_module_body of Id.t list * module_path
+  | With_definition_body of  Id.t list * constant_body
 
 and module_body =
     { mod_mp : module_path;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 0a09ad76f..fc142d253 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -123,13 +123,13 @@ type inductive_arity =
 type one_inductive_body = {
 (** {8 Primitive datas } *)
 
-    mind_typename : identifier; (** Name of the type: [Ii] *)
+    mind_typename : Id.t; (** Name of the type: [Ii] *)
 
     mind_arity_ctxt : rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *)
 
     mind_arity : inductive_arity; (** Arity sort and original user arity if monomorphic *)
 
-    mind_consnames : identifier array; (** Names of the constructors: [cij] *)
+    mind_consnames : Id.t array; (** Names of the constructors: [cij] *)
 
     mind_user_lc : types array;
  (** Types of the constructors with parameters:  [forall params, Tij],
@@ -208,8 +208,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path
-  | With_definition_body of  identifier list * constant_body
+    With_module_body of Id.t list * module_path
+  | With_definition_body of  Id.t list * constant_body
 
 and module_body =
     {  (** absolute path of the module *)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 2460ec644..db91ff597 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -37,15 +37,15 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 *)
 
 type one_inductive_entry = {
-  mind_entry_typename : identifier;
+  mind_entry_typename : Id.t;
   mind_entry_arity : constr;
-  mind_entry_consnames : identifier list;
+  mind_entry_consnames : Id.t list;
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
   mind_entry_record : bool;
   mind_entry_finite : bool;
-  mind_entry_params : (identifier * local_entry) list;
+  mind_entry_params : (Id.t * local_entry) list;
   mind_entry_inds : one_inductive_entry list }
 
 (** {6 Constants (Definition/Axiom) } *)
@@ -73,8 +73,8 @@ type module_struct_entry =
   | MSEapply of module_struct_entry * module_struct_entry
 
 and with_declaration =
-    With_Module of identifier list * module_path
-  | With_Definition of identifier list * constr
+    With_Module of Id.t list * module_path
+  | With_Definition of Id.t list * constr
 
 and module_entry =
     { mod_entry_type : module_struct_entry option;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 20436cbe7..27b7c76b4 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -238,12 +238,12 @@ let global_vars_set env constr =
     let acc =
       match kind_of_term c with
       | Var _ | Const _ | Ind _ | Construct _ ->
-	  List.fold_right Idset.add (vars_of_global env c) acc
+	  List.fold_right Id.Set.add (vars_of_global env c) acc
       | _ ->
 	  acc in
     fold_constr filtrec acc c
   in
-    filtrec Idset.empty constr
+    filtrec Id.Set.empty constr
 
 
 (* [keep_hyps env ids] keeps the part of the section context of [env] which
@@ -254,20 +254,20 @@ let keep_hyps env needed =
   let really_needed =
     Sign.fold_named_context_reverse
       (fun need (id,copt,t) ->
-        if Idset.mem id need then
+        if Id.Set.mem id need then
           let globc =
 	    match copt with
-	      | None -> Idset.empty
+	      | None -> Id.Set.empty
 	      | Some c -> global_vars_set env c in
-	  Idset.union
+	  Id.Set.union
             (global_vars_set env t)
-	    (Idset.union globc need)
+	    (Id.Set.union globc need)
         else need)
       ~init:needed
       (named_context env) in
   Sign.fold_named_context
     (fun (id,_,_ as d) nsign ->
-      if Idset.mem id really_needed then add_named_decl d nsign
+      if Id.Set.mem id really_needed then add_named_decl d nsign
       else nsign)
     (named_context env)
     ~init:empty_named_context
@@ -322,7 +322,7 @@ let apply_to_hyp (ctxt,vals) id f =
   let rec aux rtail ctxt vals =
     match ctxt, vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
-	if id_eq idc id then
+	if Id.equal idc id then
 	  (f ctxt d rtail)::ctxt, v::vals
 	else
 	  let ctxt',vals' = aux (d::rtail) ctxt vals in
@@ -335,7 +335,7 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   let rec aux ctxt vals =
     match ctxt,vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
-	if id_eq idc id then
+	if Id.equal idc id then
 	  let sign = ctxt,vals in
 	  push_named_context_val (f d sign) sign
 	else
@@ -349,7 +349,7 @@ let insert_after_hyp (ctxt,vals) id d check =
   let rec aux ctxt vals =
     match  ctxt, vals with
     | (idc,c,ct)::ctxt', v::vals' ->
-	if id_eq idc id then begin
+	if Id.equal idc id then begin
 	  check ctxt;
 	  push_named_context_val d (ctxt,vals)
 	end else
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 51e1cfa5a..d2ca7b3da 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -88,7 +88,7 @@ val push_named_context_val  :
 
 
 (** Looks up in the context of local vars referred by names ([named_context]) 
-   raises [Not_found] if the identifier is not found *)
+   raises [Not_found] if the Id.t is not found *)
 
 val lookup_named     : variable -> env -> named_declaration
 val lookup_named_val : variable -> named_context_val -> named_declaration
@@ -162,12 +162,12 @@ val set_engagement : engagement -> env -> env
    directly as [Var id] in [c] or indirectly as a section variable
    dependent in a global reference occurring in [c] *)
 
-val global_vars_set : env -> constr -> Idset.t
+val global_vars_set : env -> constr -> Id.Set.t
 
 (** the constr must be a global reference *)
-val vars_of_global : env -> constr -> identifier list
+val vars_of_global : env -> constr -> Id.t list
 
-val keep_hyps : env -> Idset.t -> section_context
+val keep_hyps : env -> Id.Set.t -> section_context
 
 (** {5 Unsafe judgments. }
     We introduce here the pre-type of judgments, which is
@@ -212,7 +212,7 @@ val insert_after_hyp : named_context_val -> variable ->
   named_declaration ->
     (named_context -> unit) -> named_context_val
 
-val remove_hyps : identifier list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.t list -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
 
 
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1aa6e8cda..2d6317967 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -37,12 +37,12 @@ let is_constructor_head t =
 type inductive_error =
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * identifier * constr * constr * int * int
+  | NotConstructor of env * Id.t * constr * constr * int * int
   | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of identifier
-  | SameNamesConstructors of identifier
-  | SameNamesOverlap of identifier list
-  | NotAnArity of identifier
+  | SameNamesTypes of Id.t
+  | SameNamesConstructors of Id.t
+  | SameNamesOverlap of Id.t list
+  | NotAnArity of Id.t
   | BadEntry
   | LargeNonPropInductiveNotInType
 
@@ -57,10 +57,10 @@ let check_constructors_names =
   let rec check idset = function
     | [] -> idset
     | c::cl ->
-	if Idset.mem c idset then
+	if Id.Set.mem c idset then
 	  raise (InductiveError (SameNamesConstructors c))
 	else
-	  check (Idset.add c idset) cl
+	  check (Id.Set.add c idset) cl
   in
   check
 
@@ -74,13 +74,13 @@ let mind_check_names mie =
     | ind::inds ->
 	let id = ind.mind_entry_typename in
 	let cl = ind.mind_entry_consnames in
-	if Idset.mem id indset then
+	if Id.Set.mem id indset then
 	  raise (InductiveError (SameNamesTypes id))
 	else
 	  let cstset' = check_constructors_names cstset cl in
-	  check (Idset.add id indset) cstset' inds
+	  check (Id.Set.add id indset) cstset' inds
   in
-  check Idset.empty Idset.empty mie.mind_entry_inds
+  check Id.Set.empty Id.Set.empty mie.mind_entry_inds
 (* The above verification is not necessary from the kernel point of
   vue since inductive and constructors are not referred to by their
   name, but only by the name of the inductive packet and an index. *)
@@ -373,7 +373,7 @@ if Int.equal nmr 0 then 0 else
   in find 0 (n-1) (lpar,List.rev hyps)
 
 let lambda_implicit_lift n a =
-  let level = UniverseLevel.make (make_dirpath [id_of_string "implicit"]) 0 in
+  let level = UniverseLevel.make (make_dirpath [Id.of_string "implicit"]) 0 in
   let implicit_sort = mkType (Universe.make level) in
   let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
   iterate lambda_implicit n (lift n a)
@@ -597,8 +597,8 @@ let fold_inductive_blocks f =
 
 let used_section_variables env inds =
   let ids = fold_inductive_blocks
-    (fun l c -> Idset.union (Environ.global_vars_set env c) l)
-      Idset.empty inds in
+    (fun l c -> Id.Set.union (Environ.global_vars_set env c) l)
+      Id.Set.empty inds in
   keep_hyps env ids
 
 let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 4d71a81d0..0d3d1bdff 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -23,12 +23,12 @@ open Typeops
 type inductive_error =
   | NonPos of env * constr * constr
   | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * identifier * constr * constr * int * int
+  | NotConstructor of env * Id.t * constr * constr * int * int
   | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of identifier
-  | SameNamesConstructors of identifier
-  | SameNamesOverlap of identifier list
-  | NotAnArity of identifier
+  | SameNamesTypes of Id.t
+  | SameNamesConstructors of Id.t
+  | SameNamesOverlap of Id.t list
+  | NotAnArity of Id.t
   | BadEntry
   | LargeNonPropInductiveNotInType
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d1cffe867..dddac2ba0 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -178,7 +178,7 @@ let instantiate_universes env ctx ar argsorts =
   (* This is a Type with constraints *)
  else Type level
 
-exception SingletonInductiveBecomesProp of identifier
+exception SingletonInductiveBecomesProp of Id.t
 
 let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps =
   match mip.mind_arity with
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 89ba78697..abf5e6c2c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -89,7 +89,7 @@ val check_cofix : env -> cofixpoint -> unit
     parameter instantiation. This is used by the Ocaml extraction,
     which cannot handle (yet?) Prop-polymorphism. *)
 
-exception SingletonInductiveBecomesProp of identifier
+exception SingletonInductiveBecomesProp of Id.t
 
 val type_of_inductive_knowing_parameters : ?polyprop:bool ->
   env -> one_inductive_body -> types array -> types
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 084628a4e..51b4ca39c 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -29,8 +29,8 @@ type signature_mismatch_error =
   | DefinitionFieldExpected
   | ModuleFieldExpected
   | ModuleTypeFieldExpected
-  | NotConvertibleInductiveField of identifier
-  | NotConvertibleConstructorField of identifier
+  | NotConvertibleInductiveField of Id.t
+  | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
   | NotConvertibleTypeField
   | NotSameConstructorNamesField
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 99cb8144a..0d87ce88b 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -56,8 +56,8 @@ type signature_mismatch_error =
   | DefinitionFieldExpected
   | ModuleFieldExpected
   | ModuleTypeFieldExpected
-  | NotConvertibleInductiveField of identifier
-  | NotConvertibleConstructorField of identifier
+  | NotConvertibleInductiveField of Id.t
+  | NotConvertibleConstructorField of Id.t
   | NotConvertibleBodyField
   | NotConvertibleTypeField
   | NotSameConstructorNamesField
diff --git a/kernel/names.ml b/kernel/names.ml
index 1917f8f40..dad51b51f 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -24,48 +24,75 @@ open Util
 
 (** {6 Identifiers } *)
 
-type identifier = string
+module Id =
+struct
+  type t = string
+
+  let equal = String.equal
 
-let check_ident_soft x =
-  Option.iter (fun (fatal,x) ->
-      if fatal then error x else Pp.msg_warning (str x))
-    (Unicode.ident_refutation x)
-let check_ident x =
-  Option.iter (fun (_,x) -> Errors.error x) (Unicode.ident_refutation x)
+  let compare = String.compare
 
-let id_of_string s =
-  let () = check_ident_soft s in
-  let s = String.copy s in
-  String.hcons s
+  let check_soft x =
+    let iter (fatal, x) =
+      if fatal then error x else Pp.msg_warning (str x)
+    in
+    Option.iter iter (Unicode.ident_refutation x)
 
-let string_of_id id = String.copy id
+  let check x =
+    let iter (_, x) = Errors.error x in
+    Option.iter iter (Unicode.ident_refutation x)
 
-let id_ord = String.compare
+  let of_string s =
+    let () = check_soft s in
+    let s = String.copy s in
+    String.hcons s
 
-let id_eq = String.equal
+  let to_string id = String.copy id
 
-module IdOrdered =
+  module Self =
   struct
-    type t = identifier
-    let compare = id_ord
+    type t = string
+    let compare = compare
   end
 
-module Idset = Set.Make(IdOrdered)
-module Idmap =
-struct
-  include Map.Make(IdOrdered)
-  exception Finded
-  let exists f m =
-    try iter (fun a b -> if f a b then raise Finded) m ; false
-    with |Finded -> true
-  let singleton k v = add k v empty
+  module Set = Set.Make(Self)
+  module Map =
+  struct
+    include Map.Make(Self)
+    exception Finded
+    let exists f m =
+      try iter (fun a b -> if f a b then raise Finded) m ; false
+      with Finded -> true
+    let singleton k v = add k v empty
+  end
+
+  module Pred = Predicate.Make(Self)
+
+  let hcons = String.hcons
+
 end
-module Idpred = Predicate.Make(IdOrdered)
+
+(** Backward compatibility for [Id.t] *)
+
+type identifier = Id.t
+
+let id_eq = Id.equal
+let id_ord = Id.compare
+let check_ident_soft = Id.check_soft
+let check_ident = Id.check
+let string_of_id = Id.to_string
+let id_of_string = Id.of_string
+
+module Idset = Id.Set
+module Idmap = Id.Map
+module Idpred = Id.Pred
+
+(** / End of backward compatibility *)
 
 (** {6 Various types based on identifiers } *)
 
-type name = Name of identifier | Anonymous
-type variable = identifier
+type name = Name of Id.t | Anonymous
+type variable = Id.t
 
 let name_eq n1 n2 = match n1, n2 with
 | Anonymous, Anonymous -> true
@@ -78,7 +105,7 @@ let name_eq n1 n2 = match n1, n2 with
     The actual representation is reversed to optimise sharing:
     Coq.A.B is ["B";"A";"Coq"] *)
 
-type module_ident = identifier
+type module_ident = Id.t
 type dir_path = module_ident list
 
 module ModIdmap = Idmap
@@ -90,7 +117,7 @@ let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) =
   | [], _ -> -1
   | _, [] -> 1
   | id1 :: p1, id2 :: p2 ->
-    let c = id_ord id1 id2 in
+    let c = Id.compare id1 id2 in
     if Int.equal c 0 then dir_path_ord p1 p2 else c
   end
 
@@ -111,7 +138,7 @@ let string_of_dirpath = function
 (** {6 Unique names for bound modules } *)
 
 let u_number = ref 0
-type uniq_ident = int * identifier * dir_path
+type uniq_ident = int * Id.t * dir_path
 let make_uid dir s = incr u_number;(!u_number,s,dir)
  let debug_string_of_uid (i,s,p) =
  "<"(*^string_of_dirpath p ^"#"^*) ^ s ^"#"^ string_of_int i^">"
@@ -125,7 +152,7 @@ let uniq_ident_ord (x : uniq_ident) (y : uniq_ident) =
     let ans = Int.compare nl nr in
     if not (Int.equal ans 0) then ans
     else
-      let ans = id_ord idl idr in
+      let ans = Id.compare idl idr in
       if not (Int.equal ans 0) then ans
       else
         dir_path_ord dpl dpr
@@ -149,7 +176,7 @@ let id_of_mbid (_,s,_) = s
 
 (** {6 Names of structure elements } *)
 
-type label = identifier
+type label = Id.t
 
 let mk_label = id_of_string
 let string_of_label = string_of_id
@@ -389,12 +416,12 @@ module Constrmap_env = Map.Make(ConstructorOrdered_env)
 
 (* Better to have it here that in closure, since used in grammar.cma *)
 type evaluable_global_reference =
-  | EvalVarRef of identifier
+  | EvalVarRef of Id.t
   | EvalConstRef of constant
 
 let eq_egr e1 e2 = match e1, e2 with
     EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
-  | EvalVarRef id1, EvalVarRef id2 -> Int.equal (id_ord id1 id2) 0
+  | EvalVarRef id1, EvalVarRef id2 -> Int.equal (Id.compare id1 id2) 0
   | _, _ -> false
 
 (** {6 Hash-consing of name objects } *)
@@ -402,7 +429,7 @@ let eq_egr e1 e2 = match e1, e2 with
 module Hname = Hashcons.Make(
   struct
     type t = name
-    type u = identifier -> identifier
+    type u = Id.t -> Id.t
     let hashcons hident = function
       | Name id -> Name (hident id)
       | n -> n
@@ -418,7 +445,7 @@ module Hname = Hashcons.Make(
 module Hdir = Hashcons.Make(
   struct
     type t = dir_path
-    type u = identifier -> identifier
+    type u = Id.t -> Id.t
     let hashcons hident d = List.smartmap hident d
     let rec equal d1 d2 =
       (d1==d2) ||
@@ -432,7 +459,7 @@ module Hdir = Hashcons.Make(
 module Huniqid = Hashcons.Make(
   struct
     type t = uniq_ident
-    type u = (identifier -> identifier) * (dir_path -> dir_path)
+    type u = (Id.t -> Id.t) * (dir_path -> dir_path)
     let hashcons (hid,hdir) (n,s,dir) = (n,hid s,hdir dir)
     let equal ((n1,s1,dir1) as x) ((n2,s2,dir2) as y) =
       (x == y) ||
@@ -502,10 +529,9 @@ module Hconstruct = Hashcons.Make(
     let hash = Hashtbl.hash
   end)
 
-let hcons_ident = String.hcons
-let hcons_name = Hashcons.simple_hcons Hname.generate hcons_ident
-let hcons_dirpath = Hashcons.simple_hcons Hdir.generate hcons_ident
-let hcons_uid = Hashcons.simple_hcons Huniqid.generate (hcons_ident,hcons_dirpath)
+let hcons_name = Hashcons.simple_hcons Hname.generate Id.hcons
+let hcons_dirpath = Hashcons.simple_hcons Hdir.generate Id.hcons
+let hcons_uid = Hashcons.simple_hcons Huniqid.generate (Id.hcons,hcons_dirpath)
 let hcons_mp =
   Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,String.hcons)
 let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,String.hcons)
@@ -526,7 +552,7 @@ let cst_full_transparent_state = (Idpred.empty, Cpred.full)
 
 type 'a tableKey =
   | ConstKey of constant
-  | VarKey of identifier
+  | VarKey of Id.t
   | RelKey of 'a
 
 
@@ -544,7 +570,7 @@ let eq_id_key ik1 ik2 =
     if ans then Int.equal (kn_ord kn1 kn2) 0
     else ans
   | VarKey id1, VarKey id2 ->
-    Int.equal (id_ord id1 id2) 0
+    Int.equal (Id.compare id1 id2) 0
   | RelKey k1, RelKey k2 -> Int.equal k1 k2
   | _ -> false
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 0f37c8055..c0b38666b 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -8,37 +8,60 @@
 
 (** {6 Identifiers } *)
 
-type identifier
+module Id :
+sig
+  type t
+  (** Type of identifiers *)
 
-val check_ident : string -> unit
-val check_ident_soft : string -> unit
+  val equal : t -> t -> bool
+  (** Equality over identifiers *)
 
-(** Parsing and printing of identifiers *)
-val string_of_id : identifier -> string
-val id_of_string : string -> identifier
+  val compare : t -> t -> int
+  (** Comparison over identifiers *)
 
-val id_ord : identifier -> identifier -> int
-val id_eq : identifier -> identifier -> bool
+  val check : string -> unit
+  (** Check that a string may be converted to an identifier. Raise an exception
+      related to the problem when this is not the case. *)
+
+  val check_soft : string -> unit
+  (** As [check], but may raise a warning instead of failing when the string is
+      not an identifier, but is a well-formed string. *)
+
+  val of_string : string -> t
+  (** Converts a string into an identifier. *)
+
+  val to_string : t -> string
+  (** Converts a identifier into an string. *)
+
+  module Set : Set.S with type elt = t
+  (** Finite sets of identifiers. *)
+
+  module Map : sig
+    include Map.S with type key = t
+    (** FIXME: this is included in OCaml 3.12 *)
+    val exists : (key -> 'a -> bool) -> 'a t -> bool
+    val singleton : key -> 'a -> 'a t
+  end
+  (** Finite maps of identifiers. *)
+
+  module Pred : Predicate.S with type elt = t
+  (** Predicates over identifiers. *)
+
+  val hcons : t -> t
+  (** Hashconsing of identifiers. *)
 
-(** Identifiers sets and maps *)
-module Idset  : Set.S with type elt = identifier
-module Idpred : Predicate.S with type elt = identifier
-module Idmap  : sig
-  include Map.S with type key = identifier
-  val exists : (identifier -> 'a -> bool) -> 'a t -> bool
-  val singleton : key -> 'a -> 'a t
 end
 
 (** {6 Various types based on identifiers } *)
 
-type name = Name of identifier | Anonymous
-type variable = identifier
+type name = Name of Id.t | Anonymous
+type variable = Id.t
 
 val name_eq : name -> name -> bool
 
 (** {6 Directory paths = section names paths } *)
 
-type module_ident = identifier
+type module_ident = Id.t
 module ModIdmap : Map.S with type key = module_ident
 
 type dir_path
@@ -67,8 +90,8 @@ val mk_label : string -> label
 val string_of_label : label -> string
 val pr_label : label -> Pp.std_ppcmds
 
-val label_of_id : identifier -> label
-val id_of_label : label -> identifier
+val label_of_id : Id.t -> label
+val id_of_label : label -> Id.t
 
 val eq_label : label -> label -> bool
 
@@ -85,9 +108,9 @@ val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
 (** The first argument is a file name - to prevent conflict between
    different files *)
 
-val make_mbid : dir_path -> identifier -> mod_bound_id
-val repr_mbid : mod_bound_id -> int * identifier * dir_path
-val id_of_mbid : mod_bound_id -> identifier
+val make_mbid : dir_path -> Id.t -> mod_bound_id
+val repr_mbid : mod_bound_id -> int * Id.t * dir_path
+val id_of_mbid : mod_bound_id -> Id.t
 val debug_string_of_mbid : mod_bound_id -> string
 val string_of_mbid : mod_bound_id -> string
 
@@ -212,7 +235,7 @@ val eq_constructor : constructor -> constructor -> bool
 
 (** Better to have it here that in Closure, since required in grammar.cma *)
 type evaluable_global_reference =
-  | EvalVarRef of identifier
+  | EvalVarRef of Id.t
   | EvalConstRef of constant
 
 val eq_egr : evaluable_global_reference ->  evaluable_global_reference
@@ -220,7 +243,6 @@ val eq_egr : evaluable_global_reference ->  evaluable_global_reference
 
 (** {6 Hash-consing } *)
 
-val hcons_ident : identifier -> identifier
 val hcons_name : name -> name
 val hcons_dirpath : dir_path -> dir_path
 val hcons_con : constant -> constant
@@ -232,10 +254,10 @@ val hcons_construct : constructor -> constructor
 
 type 'a tableKey =
   | ConstKey of constant
-  | VarKey of identifier
+  | VarKey of Id.t
   | RelKey of 'a
 
-type transparent_state = Idpred.t * Cpred.t
+type transparent_state = Id.Pred.t * Cpred.t
 
 val empty_transparent_state : transparent_state
 val full_transparent_state : transparent_state
@@ -256,3 +278,40 @@ val eq_id_key : id_key -> id_key -> bool
 val eq_con_chk : constant -> constant -> bool
 val eq_ind_chk : inductive -> inductive -> bool
 
+(** {6 Deprecated functions. For backward compatibility. *)
+
+(** {5 Identifiers} *)
+
+type identifier = Id.t
+(** @deprecated Alias for [Id.t] *)
+
+val check_ident : string -> unit
+(** @deprecated Same as [Id.check]. *)
+
+val check_ident_soft : string -> unit
+(** @deprecated Same as [Id.check_soft]. *)
+
+val string_of_id : identifier -> string
+(** @deprecated Same as [Id.to_string]. *)
+
+val id_of_string : string -> identifier
+(** @deprecated Same as [Id.of_string]. *)
+
+val id_ord : identifier -> identifier -> int
+(** @deprecated Same as [Id.compare]. *)
+
+val id_eq : identifier -> identifier -> bool
+(** @deprecated Same as [Id.equal]. *)
+
+module Idset  : Set.S with type elt = identifier and type t = Id.Set.t
+(** @deprecated Same as [Id.Set]. *)
+
+module Idpred : Predicate.S with type elt = identifier and type t = Id.Pred.t
+(** @deprecated Same as [Id.Pred]. *)
+
+module Idmap  : sig
+  include Map.S with type key = identifier
+  val exists : (identifier -> 'a -> bool) -> 'a t -> bool
+  val singleton : key -> 'a -> 'a t
+end
+(** @deprecated Same as [Id.Map]. *)
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 207a37f97..2a467ad0a 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -39,12 +39,12 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of values * Idset.t
+    | VKvalue of values * Id.Set.t
     | VKnone
 
 type lazy_val = val_kind ref
 
-type named_vals = (identifier * lazy_val) list
+type named_vals = (Id.t * lazy_val) list
 
 type env = {
   env_globals       : globals;
@@ -116,7 +116,7 @@ let push_named d env =
       env_named_vals =  (id,rval):: env.env_named_vals }
 
 let lookup_named_val id env =
-  snd(List.find (fun (id',_) -> id_eq id id') env.env_named_vals)
+  snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals)
 
 (* Warning all the names should be different *)
 let env_of_named id env = env
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index a8868a4f8..569e8830a 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -31,12 +31,12 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of values * Idset.t
+    | VKvalue of values * Id.Set.t
     | VKnone
 
 type lazy_val = val_kind ref
 
-type named_vals = (identifier * lazy_val) list
+type named_vals = (Id.t * lazy_val) list
 
 type env = {
     env_globals       : globals;
@@ -66,8 +66,8 @@ val env_of_rel     : int -> env -> env
 val push_named_context_val  :
     named_declaration -> named_context_val -> named_context_val
 val push_named       : named_declaration -> env -> env
-val lookup_named_val : identifier -> env -> lazy_val
-val env_of_named     : identifier -> env -> env
+val lookup_named_val : Id.t -> env -> lazy_val
+val env_of_named     : Id.t -> env -> env
 
 (** Global constants *)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index fb6ffd2d1..9aa70c9eb 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -26,7 +26,7 @@ open Esubst
 
 let unfold_reference ((ids, csts), infos) k =
   match k with
-    | VarKey id when not (Idpred.mem id ids) -> None
+    | VarKey id when not (Id.Pred.mem id ids) -> None
     | ConstKey cst when not (Cpred.mem cst csts) -> None
     | _ -> unfold_reference infos k
 
@@ -446,7 +446,7 @@ let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->No
 let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars
 let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars
 
-let fconv = trans_fconv (Idpred.full, Cpred.full)
+let fconv = trans_fconv (Id.Pred.full, Cpred.full)
 
 let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
 let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 28052c41b..8a95c9fd2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -242,7 +242,7 @@ let safe_push_named (id,_,_ as d) env =
   let _ =
     try
       let _ = lookup_named id env in
-      error ("Identifier "^string_of_id id^" already defined.")
+      error ("Identifier "^Id.to_string id^" already defined.")
     with Not_found -> () in
   Environ.push_named d env
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 34dc68d2e..71ebe15ce 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -31,10 +31,10 @@ val is_empty : safe_environment -> bool
 
 (** Adding and removing local declarations (Local or Variables) *)
 val push_named_assum :
-  identifier * types -> safe_environment ->
+  Id.t * types -> safe_environment ->
     Univ.constraints * safe_environment
 val push_named_def :
-  identifier * constr * types option -> safe_environment ->
+  Id.t * constr * types option -> safe_environment ->
     Univ.constraints * safe_environment
 
 (** Adding global axioms or definitions *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index b2a509678..3fced7119 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -29,7 +29,7 @@ let empty_named_context = []
 let add_named_decl d sign = d::sign
 
 let rec lookup_named id = function
-  | (id',_,_ as decl) :: _ when id_eq id id' -> decl
+  | (id',_,_ as decl) :: _ when Id.equal id id' -> decl
   | _ :: sign -> lookup_named id sign
   | [] -> raise Not_found
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 4325fe90c..6239ab5dc 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -16,9 +16,9 @@ type section_context = named_context
 
 val empty_named_context : named_context
 val add_named_decl : named_declaration -> named_context -> named_context
-val vars_of_named_context : named_context -> identifier list
+val vars_of_named_context : named_context -> Id.t list
 
-val lookup_named : identifier -> named_context -> named_declaration
+val lookup_named : Id.t -> named_context -> named_declaration
 
 (** number of declarations *)
 val named_context_length : named_context -> int
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6aaf5b47d..d278c2d0c 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -136,8 +136,8 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 
   let check_packet cst p1 p2 =
     let check f test why = if not (test (f p1) (f p2)) then error why in
-      check (fun p -> p.mind_consnames) (Array.equal id_eq) NotSameConstructorNamesField;
-      check (fun p -> p.mind_typename) id_eq NotSameInductiveNameInBlockField;
+      check (fun p -> p.mind_consnames) (Array.equal Id.equal) NotSameConstructorNamesField;
+      check (fun p -> p.mind_typename) Id.equal NotSameInductiveNameInBlockField;
       (* nf_lc later *)
       (* nf_arity later *)
       (* user_lc ignored *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 2ad39d189..ced5c6fc5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -105,7 +105,7 @@ type ('constr, 'types) pcofixpoint =
    de Bruijn indices. *)
 type ('constr, 'types) kind_of_term =
   | Rel       of int
-  | Var       of identifier
+  | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
@@ -345,7 +345,7 @@ let isRelN n c = match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false
 
 (* Tests if a variable *)
 let isVar c = match kind_of_term c with Var _ -> true | _ -> false
-let isVarId id c = match kind_of_term c with Var id' -> Int.equal (id_ord id id') 0 | _ -> false
+let isVarId id c = match kind_of_term c with Var id' -> Int.equal (Id.compare id id') 0 | _ -> false
 
 (* Tests if an inductive *)
 let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
@@ -578,7 +578,7 @@ let compare_constr f t1 t2 =
   match kind_of_term t1, kind_of_term t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
-  | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0
+  | Var id1, Var id2 -> Int.equal (Id.compare id1 id2) 0
   | Sort s1, Sort s2 -> Int.equal (sorts_ord s1 s2) 0
   | Cast (c1,_,_), _ -> f c1 t2
   | _, Cast (c2,_,_) -> f t1 c2
@@ -624,7 +624,7 @@ let constr_ord_int f t1 t2 =
   match kind_of_term t1, kind_of_term t2 with
     | Rel n1, Rel n2 -> Int.compare n1 n2
     | Meta m1, Meta m2 -> Int.compare m1 m2
-    | Var id1, Var id2 -> id_ord id1 id2
+    | Var id1, Var id2 -> Id.compare id1 id2
     | Sort s1, Sort s2 -> sorts_ord s1 s2
     | Cast (c1,_,_), _ -> f c1 t2
     | _, Cast (c2,_,_) -> f t1 c2
@@ -669,7 +669,7 @@ type types = constr
 
 type strategy = types option
 
-type named_declaration = identifier * constr option * types
+type named_declaration = Id.t * constr option * types
 type rel_declaration = name * constr option * types
 
 let map_named_declaration f (id, (v : strategy), ty) = (id, Option.map f v, f ty)
@@ -685,7 +685,7 @@ let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
 let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
 
 let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
-  id_eq i1 i2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
+  Id.equal i1 i2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
 
 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
   name_eq n1 n2 && Option.equal eq_constr c1 c2 && eq_constr t1 t2
@@ -856,7 +856,7 @@ let subst1_named_decl = subst1_decl
 let rec thin_val = function
   | [] -> []
   | (((id,{ sit = v }) as s)::tl) when isVar v ->
-      if Int.equal (id_ord id (destVar v)) 0 then thin_val tl else s::(thin_val tl)
+      if Int.equal (Id.compare id (destVar v)) 0 then thin_val tl else s::(thin_val tl)
   | h::tl -> h::(thin_val tl)
 
 (* (replace_vars sigma M) applies substitution sigma to term M *)
@@ -1433,7 +1433,7 @@ let hcons_constr =
      hcons_ind,
      hcons_con,
      hcons_name,
-     hcons_ident)
+     Id.hcons)
 
 let hcons_types = hcons_constr
 
diff --git a/kernel/term.mli b/kernel/term.mli
index cb48fbbe3..17c55f069 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -79,7 +79,7 @@ type types = constr
 val mkRel : int -> constr
 
 (** Constructs a Variable *)
-val mkVar : identifier -> constr
+val mkVar : Id.t -> constr
 
 (** Constructs an patvar named "?n" *)
 val mkMeta : metavariable -> constr
@@ -104,7 +104,7 @@ val mkCast : constr * cast_kind * constr -> constr
 
 (** Constructs the product [(x:t1)t2] *)
 val mkProd : name * types * types -> types
-val mkNamedProd : identifier -> types -> types -> types
+val mkNamedProd : Id.t -> types -> types -> types
 
 (** non-dependent product [t1 -> t2], an alias for
    [forall (_:t1), t2]. Beware [t_2] is NOT lifted.
@@ -114,11 +114,11 @@ val mkArrow : types -> types -> constr
 
 (** Constructs the abstraction \[x:t{_ 1}\]t{_ 2} *)
 val mkLambda : name * types * constr -> constr
-val mkNamedLambda : identifier -> types -> constr -> constr
+val mkNamedLambda : Id.t -> types -> constr -> constr
 
 (** Constructs the product [let x = t1 : t2 in t3] *)
 val mkLetIn : name * constr * types * constr -> constr
-val mkNamedLetIn : identifier -> constr -> types -> constr -> constr
+val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
 
 (** [mkApp (f,[| t_1; ...; t_n |]] constructs the application
    {% $(f~t_1~\dots~t_n)$ %}. *)
@@ -197,7 +197,7 @@ type ('constr, 'types) pcofixpoint =
 
 type ('constr, 'types) kind_of_term =
   | Rel       of int
-  | Var       of identifier
+  | Var       of Id.t
   | Meta      of metavariable
   | Evar      of 'constr pexistential
   | Sort      of sorts
@@ -234,7 +234,7 @@ val kind_of_type : types -> (constr, types) kind_of_type
 val isRel  : constr -> bool
 val isRelN : int -> constr -> bool
 val isVar  : constr -> bool
-val isVarId : identifier -> constr -> bool
+val isVarId : Id.t -> constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
@@ -271,7 +271,7 @@ val destRel : constr -> int
 val destMeta : constr -> metavariable
 
 (** Destructs a variable *)
-val destVar : constr -> identifier
+val destVar : constr -> Id.t
 
 (** Destructs a sort. [is_Prop] recognizes the sort {% \textsf{%}Prop{% }%}, whether
    [isprop] recognizes both {% \textsf{%}Prop{% }%} and {% \textsf{%}Set{% }%}. *)
@@ -337,7 +337,7 @@ val destCoFix : constr -> cofixpoint
     (in the latter case, [na] is of type [name] but just for printing
     purpose) *)
 
-type named_declaration = identifier * constr option * types
+type named_declaration = Id.t * constr option * types
 type rel_declaration = name * constr option * types
 
 val map_named_declaration :
@@ -570,16 +570,16 @@ val subst1_decl : constr -> rel_declaration -> rel_declaration
 val subst1_named_decl : constr -> named_declaration -> named_declaration
 val substl_named_decl : constr list -> named_declaration -> named_declaration
 
-val replace_vars : (identifier * constr) list -> constr -> constr
-val subst_var : identifier -> constr -> constr
+val replace_vars : (Id.t * constr) list -> constr -> constr
+val subst_var : Id.t -> constr -> constr
 
 (** [subst_vars [id1;...;idn] t] substitute [VAR idj] by [Rel j] in [t]
    if two names are identical, the one of least indice is kept *)
-val subst_vars : identifier list -> constr -> constr
+val subst_vars : Id.t list -> constr -> constr
 
 (** [substn_vars n [id1;...;idn] t] substitute [VAR idj] by [Rel j+n-1] in [t]
    if two names are identical, the one of least indice is kept *)
-val substn_vars : int -> identifier list -> constr -> constr
+val substn_vars : int -> Id.t list -> constr -> constr
 
 
 (** {6 Functionals working on the immediate subterm of a construction } *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index aed7615b8..ccb6a4a7d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -62,7 +62,7 @@ let safe_push_named (id,_,_ as d) env =
   let _ =
     try
       let _ = lookup_named id env in
-      error ("Identifier "^string_of_id id^" already defined.")
+      error ("Identifier "^Id.to_string id^" already defined.")
     with Not_found -> () in
   push_named d env
 
@@ -110,28 +110,28 @@ let global_vars_set_constant_type env = function
   | PolymorphicArity (ctx,_) ->
       Sign.fold_rel_context
         (fold_rel_declaration
-	  (fun t c -> Idset.union (global_vars_set env t) c))
-      ctx ~init:Idset.empty
+	  (fun t c -> Id.Set.union (global_vars_set env t) c))
+      ctx ~init:Id.Set.empty
 
 let build_constant_declaration env kn (def,typ,cst,ctx) =
   let hyps = 
     let inferred =
       let ids_typ = global_vars_set_constant_type env typ in
       let ids_def = match def with
-      | Undef _ -> Idset.empty
+      | Undef _ -> Id.Set.empty
       | Def cs -> global_vars_set env (Declarations.force cs)
       | OpaqueDef lc -> 
           global_vars_set env (Declarations.force_opaque lc) in
-      keep_hyps env (Idset.union ids_typ ids_def) in
+      keep_hyps env (Id.Set.union ids_typ ids_def) in
     let declared = match ctx with
       | None -> inferred 
       | Some declared -> declared in
-    let mk_set l = List.fold_right Idset.add (List.map pi1 l) Idset.empty in
+    let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
-    if not (Idset.subset inferred_set declared_set) then
+    if not (Id.Set.subset inferred_set declared_set) then
       error ("The following section variable are used but not declared:\n"^
-        (String.concat ", " (List.map string_of_id
-          (Idset.elements (Idset.diff inferred_set declared_set)))));
+        (String.concat ", " (List.map Id.to_string
+          (Id.Set.elements (Id.Set.diff inferred_set declared_set)))));
     declared in
   let tps = Cemitcodes.from_val (compile_constant_body env def) in
   { const_hyps = hyps;
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 3a4179fd4..7b3aff20d 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -20,7 +20,7 @@ val infer_v    : env -> constr array -> unsafe_judgment array * constraints
 val infer_type : env -> types        -> unsafe_type_judgment * constraints
 
 val infer_local_decls :
-  env -> (identifier * local_entry) list
+  env -> (Id.t * local_entry) list
     -> env * rel_context * constraints
 
 (** {6 Basic operations of the typing machine. } *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 5f2e32a5d..1d71fd672 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -776,7 +776,7 @@ let bellman_ford bottom g =
     graph already contains [Type.n] nodes (calling a module Type is
     probably a bad idea anyway). *)
 let sort_universes orig =
-  let mp = Names.make_dirpath [Names.id_of_string "Type"] in
+  let mp = Names.make_dirpath [Names.Id.of_string "Type"] in
   let rec make_level accu g i =
     let type0 = UniverseLevel.Level (i, mp) in
     let distances = bellman_ford type0 g in
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 4bdc1fbff..cbc68c488 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -54,7 +54,7 @@ type whd =
 
 val val_of_str_const : structured_constant -> values
 val val_of_rel : int -> values
-val val_of_named : identifier -> values
+val val_of_named : Id.t -> values
 val val_of_constant : constant -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"