Modulification of identifier

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

29 files changed, 210 insertions, 210 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 3fc4aa84f..eaca147e1 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -126,15 +126,15 @@ let build_beq_scheme kn =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   (* predef coq's boolean type *)
   (* rec name *)
-  let rec_name i =(string_of_id (Array.get mib.mind_packets i).mind_typename)^
+  let rec_name i =(Id.to_string (Array.get mib.mind_packets i).mind_typename)^
                     "_eqrec"
   in
   (* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *)
   let create_input c =
     let myArrow u v = mkArrow u (lift 1 v)
     and eqName = function
-        | Name s -> id_of_string ("eq_"^(string_of_id s))
-        | Anonymous -> id_of_string "eq_A"
+        | Name s -> Id.of_string ("eq_"^(Id.to_string s))
+        | Anonymous -> Id.of_string "eq_A"
     in
     let ext_rel_list = extended_rel_list 0 lnamesparrec in
       let lift_cnt = ref 0 in
@@ -154,7 +154,7 @@ let build_beq_scheme kn =
         List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *)
           (* Same here , hoping the auto renaming will do something good ;)  *)
           mkNamedLambda
-                (match n with Name s -> s | Anonymous ->  id_of_string "A")
+                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
                 t  a) eq_input lnamesparrec
  in
  let make_one_eq cur =
@@ -178,7 +178,7 @@ let build_beq_scheme kn =
 	let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
 	match kind_of_term c with
         | Rel x -> mkRel (x-nlist+ndx)
-        | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x)))
+        | Var x -> mkVar (Id.of_string ("eq_"^(Id.to_string x)))
         | Cast (x,_,_) -> aux (applist (x,a))
         | App _ -> assert false
         | Ind (kn',i as ind') -> if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
@@ -265,18 +265,18 @@ let build_beq_scheme kn =
 
 	  ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
 			(mkCase (ci,do_predicate rel_list nb_cstr_args,
-				  mkVar (id_of_string "Y") ,ar2))
+				  mkVar (Id.of_string "Y") ,ar2))
 			 (constrsi.(i).cs_args))
 	done;
-        mkNamedLambda (id_of_string "X") (mkFullInd ind (nb_ind-1+1))  (
-          mkNamedLambda (id_of_string "Y") (mkFullInd ind (nb_ind-1+2))  (
- 	    mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar)))
+        mkNamedLambda (Id.of_string "X") (mkFullInd ind (nb_ind-1+1))  (
+          mkNamedLambda (Id.of_string "Y") (mkFullInd ind (nb_ind-1+2))  (
+ 	    mkCase (ci, do_predicate rel_list 0,mkVar (Id.of_string "X"),ar)))
     in (* build_beq_scheme *)
     let names = Array.make nb_ind Anonymous and
         types = Array.make nb_ind mkSet and
         cores = Array.make nb_ind mkSet in
     for i=0 to (nb_ind-1) do
-        names.(i) <- Name (id_of_string (rec_name i));
+        names.(i) <- Name (Id.of_string (rec_name i));
 	types.(i) <- mkArrow (mkFullInd (kn,i) 0)
                      (mkArrow (mkFullInd (kn,i) 1) bb);
         cores.(i) <- make_one_eq i
@@ -319,9 +319,9 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
     let s = destVar v in
     let n = Array.length avoid in
     let rec find i =
-      if id_eq avoid.(n-i) s then avoid.(n-i-x)
+      if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else error ("Var "^(string_of_id s)^" seems unknown.")
+            else error ("Var "^(Id.to_string s)^" seems unknown.")
       )
     in mkVar (find 1)
   with _ -> (* if this happen then the args have to be already declared as a
@@ -366,9 +366,9 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
     let s = destVar v in
     let n = Array.length avoid in
     let rec find i =
-      if id_eq avoid.(n-i) s then avoid.(n-i-x)
+      if Id.equal avoid.(n-i) s then avoid.(n-i-x)
       else (if i<n then find (i+1)
-            else error ("Var "^(string_of_id s)^" seems unknown.")
+            else error ("Var "^(Id.to_string s)^" seems unknown.")
       )
     in mkVar (find 1)
   with _ -> (* if this happen then the args have to be already declared as a
@@ -444,11 +444,11 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
 *)
 let list_id l = List.fold_left ( fun a (n,_,t) -> let s' =
       match n with
-        Name s -> string_of_id s
+        Name s -> Id.to_string s
       | Anonymous -> "A" in
-          (id_of_string s',id_of_string ("eq_"^s'),
-              id_of_string (s'^"_bl"),
-              id_of_string (s'^"_lb"))
+          (Id.of_string s',Id.of_string ("eq_"^s'),
+              Id.of_string (s'^"_bl"),
+              Id.of_string (s'^"_lb"))
             ::a
     ) [] l
 (*
@@ -470,8 +470,8 @@ let compute_bl_goal ind lnamesparrec nparrec =
   let eqI = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
   let create_input c =
-    let x = id_of_string "x" and
-        y = id_of_string "y" in
+    let x = Id.of_string "x" and
+        y = Id.of_string "y" in
       let bl_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd x (mkVar s) (
             mkNamedProd y (mkVar s) (
@@ -490,11 +490,11 @@ let compute_bl_goal ind lnamesparrec nparrec =
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
       List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  id_of_string "A")
+                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
                 t  a) eq_input lnamesparrec
     in
-      let n = id_of_string "x" and
-          m = id_of_string "y" in
+      let n = Id.of_string "x" and
+          m = Id.of_string "y" in
      create_input (
         mkNamedProd n (mkFullInd ind nparrec) (
           mkNamedProd m (mkFullInd ind (nparrec+1)) (
@@ -514,11 +514,11 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
       let fresh_first_intros = List.map ( fun s ->
         let fresh = fresh_id (!avoid) s gsig in
         avoid := fresh::(!avoid); fresh ) first_intros in
-      let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
+      let freshn = fresh_id (!avoid) (Id.of_string "x") gsig in
       let freshm = avoid := freshn::(!avoid);
-            fresh_id (!avoid) (id_of_string "y") gsig in
+            fresh_id (!avoid) (Id.of_string "y") gsig in
       let freshz = avoid := freshm::(!avoid);
-            fresh_id (!avoid) (id_of_string "Z") gsig in
+            fresh_id (!avoid) (Id.of_string "Z") gsig in
   (* try with *)
       avoid := freshz::(!avoid);
       tclTHENSEQ [ intros_using fresh_first_intros;
@@ -539,7 +539,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                       tclTHENSEQ [
                          simple_apply_in freshz (andb_prop());
                          fun gl ->
-                           let fresht = fresh_id (!avoid) (id_of_string "Z") gsig
+                           let fresht = fresh_id (!avoid) (Id.of_string "Z") gsig
                            in
                             avoid := fresht::(!avoid);
                             (new_destruct false [Tacexpr.ElimOnConstr
@@ -600,8 +600,8 @@ let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eqI = eqI ind lnamesparrec in
     let create_input c =
-      let x = id_of_string "x" and
-          y = id_of_string "y" in
+      let x = Id.of_string "x" and
+          y = Id.of_string "y" in
       let lb_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd x (mkVar s) (
             mkNamedProd y (mkVar s) (
@@ -620,11 +620,11 @@ let compute_lb_goal ind lnamesparrec nparrec =
         mkNamedProd seq b a
       ) lb_input (List.rev list_id) (List.rev eqs_typ) in
       List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  id_of_string "A")
+                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
                 t  a) eq_input lnamesparrec
     in
-      let n = id_of_string "x" and
-          m = id_of_string "y" in
+      let n = Id.of_string "x" and
+          m = Id.of_string "y" in
       create_input (
         mkNamedProd n (mkFullInd ind nparrec) (
           mkNamedProd m (mkFullInd ind (nparrec+1)) (
@@ -644,11 +644,11 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
       let fresh_first_intros = List.map ( fun s ->
         let fresh = fresh_id (!avoid) s gsig in
         avoid := fresh::(!avoid); fresh ) first_intros in
-      let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
+      let freshn = fresh_id (!avoid) (Id.of_string "x") gsig in
       let freshm = avoid := freshn::(!avoid);
-            fresh_id (!avoid) (id_of_string "y") gsig in
+            fresh_id (!avoid) (Id.of_string "y") gsig in
       let freshz = avoid := freshm::(!avoid);
-            fresh_id (!avoid) (id_of_string "Z") gsig in
+            fresh_id (!avoid) (Id.of_string "Z") gsig in
   (* try with *)
       avoid := freshz::(!avoid);
       tclTHENSEQ [ intros_using fresh_first_intros;
@@ -716,8 +716,8 @@ let compute_dec_goal ind lnamesparrec nparrec =
   check_not_is_defined ();
   let list_id = list_id lnamesparrec in
     let create_input c =
-      let x = id_of_string "x" and
-          y = id_of_string "y" in
+      let x = Id.of_string "x" and
+          y = Id.of_string "y" in
       let lb_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd x (mkVar s) (
             mkNamedProd y (mkVar s) (
@@ -749,11 +749,11 @@ let compute_dec_goal ind lnamesparrec nparrec =
         mkNamedProd seq b a
       ) bl_input (List.rev list_id) (List.rev eqs_typ) in
       List.fold_left (fun a (n,_,t) -> mkNamedProd
-                (match n with Name s -> s | Anonymous ->  id_of_string "A")
+                (match n with Name s -> s | Anonymous ->  Id.of_string "A")
                 t  a) eq_input lnamesparrec
     in
-      let n = id_of_string "x" and
-          m = id_of_string "y" in
+      let n = Id.of_string "x" and
+          m = Id.of_string "y" in
         let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
         create_input (
           mkNamedProd n (mkFullInd ind (2*nparrec)) (
@@ -778,11 +778,11 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
   let fresh_first_intros = List.map ( fun s ->
     let fresh = fresh_id (!avoid) s gsig in
     avoid := fresh::(!avoid); fresh ) first_intros in
-  let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
+  let freshn = fresh_id (!avoid) (Id.of_string "x") gsig in
   let freshm = avoid := freshn::(!avoid);
-    fresh_id (!avoid) (id_of_string "y") gsig in
+    fresh_id (!avoid) (Id.of_string "y") gsig in
   let freshH = avoid := freshm::(!avoid);
-    fresh_id (!avoid) (id_of_string "H") gsig in
+    fresh_id (!avoid) (Id.of_string "H") gsig in
   let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
   avoid := freshH::(!avoid);
   let arfresh = Array.of_list fresh_first_intros in
@@ -806,7 +806,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
 	)
 	  (tclTHEN (destruct_on eqbnm) Auto.default_auto);
         (fun gsig ->
-	  let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in
+	  let freshH2 = fresh_id (!avoid) (Id.of_string "H") gsig in
           avoid := freshH2::(!avoid);
 	  tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
 	    (* left *)
@@ -817,7 +817,7 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
             ];
 	    (*right *)
             (fun gsig ->
-	    let freshH3 = fresh_id (!avoid) (id_of_string "H") gsig in
+	    let freshH3 = fresh_id (!avoid) (Id.of_string "H") gsig in
             avoid := freshH3::(!avoid);
             tclTHENSEQ [
 	      simplest_right ;
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 37496387e..2d1e1c6a3 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.ml
@@ -32,7 +32,7 @@ open Vernacexpr
 type info = {
   label : int;
   nproofs : int;
-  prfname : identifier option;
+  prfname : Id.t option;
   prfdepth : int;
   ngoals : int;
   cmd : vernac_expr;
@@ -228,7 +228,7 @@ let get_script prf =
   let script = ref [] in
   let select i = match i.prfname with
     | None -> raise Not_found
-    | Some p when id_eq p prf && i.reachable -> script := i :: !script
+    | Some p when Id.equal p prf && i.reachable -> script := i :: !script
     | _ -> ()
   in
   (try Stack.iter select history with Not_found -> ());
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
index d350901e6..5f9e9f98c 100644
--- a/toplevel/backtrack.mli
+++ b/toplevel/backtrack.mli
@@ -66,7 +66,7 @@ val reset_initial : unit -> unit
 
 (** Reset to the last known state just before defining [id] *)
 
-val reset_name : Names.identifier Loc.located -> unit
+val reset_name : Names.Id.t Loc.located -> unit
 
 (** When a proof is ended (via either Qed/Admitted/Restart/Abort),
     old proof steps should be marked differently to avoid jumping back
@@ -77,11 +77,11 @@ val reset_name : Names.identifier Loc.located -> unit
     We also mark as unreachable the proof steps cancelled via a Undo.
 *)
 
-val mark_unreachable : ?after:int -> Names.identifier list -> unit
+val mark_unreachable : ?after:int -> Names.Id.t list -> unit
 
 (** Parse the history stack for printing the script of a proof *)
 
-val get_script : Names.identifier -> (Vernacexpr.vernac_expr * int) list
+val get_script : Names.Id.t -> (Vernacexpr.vernac_expr * int) list
 
 
 (** For debug purpose, a dump of the history *)
@@ -89,7 +89,7 @@ val get_script : Names.identifier -> (Vernacexpr.vernac_expr * int) list
 type info = {
   label : int;
   nproofs : int;
-  prfname : Names.identifier option;
+  prfname : Names.Id.t option;
   prfdepth : int;
   ngoals : int;
   cmd : Vernacexpr.vernac_expr;
diff --git a/toplevel/class.ml b/toplevel/class.ml
index aa77a00c5..01205e597 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -166,7 +166,7 @@ let ident_key_of_class = function
   | CL_SORT -> "Sortclass"
   | CL_CONST sp -> string_of_label (con_label sp)
   | CL_IND (sp,_) -> string_of_label (mind_label sp)
-  | CL_SECVAR id -> string_of_id id
+  | CL_SECVAR id -> Id.to_string id
 
 (* coercion identité *)
 
@@ -185,7 +185,7 @@ let build_id_coercion idf_opt source =
   let lams,t = decompose_lam_assum c in
   let val_f =
     it_mkLambda_or_LetIn
-      (mkLambda (Name (id_of_string "x"),
+      (mkLambda (Name (Id.of_string "x"),
 		 applistc vs (extended_rel_list 0 lams),
 		 mkRel 1))
        lams
@@ -209,7 +209,7 @@ let build_id_coercion idf_opt source =
       | Some idf -> idf
       | None ->
 	  let cl,_ = find_class_type Evd.empty t in
-	  id_of_string ("Id_"^(ident_key_of_class source)^"_"^
+	  Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
                         (ident_key_of_class cl))
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
@@ -290,7 +290,7 @@ let try_add_new_coercion_with_source ref stre ~source =
 let add_coercion_hook stre ref =
   try_add_new_coercion ref stre;
   Flags.if_verbose msg_info
-    (pr_global_env Idset.empty ref ++ str " is now a coercion")
+    (pr_global_env Id.Set.empty ref ++ str " is now a coercion")
 
 let add_subclass_hook stre ref =
   let cl = class_of_global ref in
diff --git a/toplevel/class.mli b/toplevel/class.mli
index e4ff43972..a72ec1a81 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -39,7 +39,7 @@ val try_add_new_coercion_with_source : global_reference -> locality ->
 (** [try_add_new_identity_coercion id s src tg] enriches the
    environment with a new definition of name [id] declared as an
    identity coercion from [src] to [tg] *)
-val try_add_new_identity_coercion : identifier -> locality ->
+val try_add_new_identity_coercion : Id.t -> locality ->
   source:cl_typ -> target:cl_typ -> unit
 
 val add_coercion_hook : unit Tacexpr.declaration_hook
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 618ec2bc0..fbabaa432 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -63,7 +63,7 @@ let existing_instance glob g =
 let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
 let mismatched_props env n m = mismatched_ctx_inst env Properties n m
 
-type binder_list = (identifier Loc.located * bool * constr_expr) list
+type binder_list = (Id.t Loc.located * bool * constr_expr) list
 
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
@@ -121,7 +121,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
   let tclass, ids =
     match bk with
     | Implicit ->
-	Implicit_quantifiers.implicit_application Idset.empty ~allow_partial:false
+	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
 	  (fun avoid (clname, (id, _, t)) ->
 	    match clname with
 	    | Some (cl, b) ->
@@ -129,7 +129,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
-    | Explicit -> cl, Idset.empty
+    | Explicit -> cl, Id.Set.empty
   in
   let tclass = if generalize then CGeneralization (Loc.ghost, Implicit, Some AbsPi, tclass) else tclass in
   let k, cty, ctx', ctx, len, imps, subst =
@@ -210,7 +210,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		   if Option.is_empty b then
 		     try
                       let is_id (id', _) = match id, get_id id' with
-                      | Name id, (_, id') -> id_eq id id'
+                      | Name id, (_, id') -> Id.equal id id'
                       | Anonymous, _ -> false
                       in
 		       let (loc_mid, c) =
@@ -338,7 +338,7 @@ let context l =
     else (
       let impl = List.exists 
 	(fun (x,_) ->
-	   match x with ExplByPos (_, Some id') -> id_eq id id' | _ -> false) impls
+	   match x with ExplByPos (_, Some id') -> Id.equal id id' | _ -> false) impls
       in
 	Command.declare_assumption false (Local (* global *), Definitional) t
 	  [] impl (* implicit *) None (* inline *) (Loc.ghost, id) && status)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index cfb8362f0..736ba62a9 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -40,10 +40,10 @@ val declare_instance_constant :
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
-  identifier -> (** name *)
+  Id.t -> (** name *)
   Term.constr -> (** body *)
   Term.types -> (** type *)
-  Names.identifier
+  Names.Id.t
 
 val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)
@@ -55,7 +55,7 @@ val new_instance :
   ?tac:Proof_type.tactic  ->
   ?hook:(Globnames.global_reference -> unit) ->
   int option ->
-  identifier
+  Id.t
 
 (** Setting opacity *)
 
@@ -63,7 +63,7 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 
 (** For generation on names based on classes only *)
 
-val id_of_class : typeclass -> identifier
+val id_of_class : typeclass -> Id.t
 
 (** Context command *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c6c934a81..fc039d968 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -210,9 +210,9 @@ let push_types env idl tl =
     env idl tl
 
 type structured_one_inductive_expr = {
-  ind_name : identifier;
+  ind_name : Id.t;
   ind_arity : constr_expr;
-  ind_lc : (identifier * constr_expr) list
+  ind_lc : (Id.t * constr_expr) list
 }
 
 type structured_inductive_expr =
@@ -430,7 +430,7 @@ let rec partial_order = function
 	    let res = List.remove_assoc y res in
 	    let res = List.map (function
 	      | (z, Inl t) ->
-		  if id_eq t y then (z, Inl x) else (z, Inl t)
+		  if Id.equal t y then (z, Inl x) else (z, Inl t)
 	      | (z, Inr zge) ->
 		  if List.mem y zge then
 		    (z, Inr (List.add_set x (List.remove y zge)))
@@ -446,11 +446,11 @@ let rec partial_order = function
 let non_full_mutual_message x xge y yge isfix rest =
   let reason =
     if List.mem x yge then
-      string_of_id y^" depends on "^string_of_id x^" but not conversely"
+      Id.to_string y^" depends on "^Id.to_string x^" but not conversely"
     else if List.mem y xge then
-      string_of_id x^" depends on "^string_of_id y^" but not conversely"
+      Id.to_string x^" depends on "^Id.to_string y^" but not conversely"
     else
-      string_of_id y^" and "^string_of_id x^" are not mutually dependent" in
+      Id.to_string y^" and "^Id.to_string x^" are not mutually dependent" in
   let e = if List.is_empty rest then reason else "e.g.: "^reason in
   let k = if isfix then "fixpoint" else "cofixpoint" in
   let w =
@@ -464,7 +464,7 @@ let check_mutuality env isfix fixl =
   let names = List.map fst fixl in
   let preorder =
     List.map (fun (id,def) ->
-      (id, List.filter (fun id' -> not (id_eq id id') && occur_var env id' def) names))
+      (id, List.filter (fun id' -> not (Id.equal id id') && occur_var env id' def) names))
       fixl in
   let po = partial_order preorder in
   match List.filter (function (_,Inr _) -> true | _ -> false) po with
@@ -473,8 +473,8 @@ let check_mutuality env isfix fixl =
     | _ -> ()
 
 type structured_fixpoint_expr = {
-  fix_name : identifier;
-  fix_annot : identifier Loc.located option;
+  fix_name : Id.t;
+  fix_annot : Id.t Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
@@ -532,7 +532,7 @@ let compute_possible_guardness_evidences (ids,_,na) =
       List.interval 0 (List.length ids - 1)
 
 type recursive_preentry =
-  identifier list * constr option list * types list
+  Id.t list * constr option list * types list
 
 (* Wellfounded definition *)
 
@@ -597,7 +597,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
   let top_arity = interp_type_evars isevars top_env arityc in
   let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
   let argtyp, letbinders, make = telescope binders_rel in
-  let argname = id_of_string "recarg" in
+  let argname = Id.of_string "recarg" in
   let arg = (Name argname, None, argtyp) in
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
@@ -631,7 +631,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     in wf_rel, wf_rel_fun, measure
   in
   let wf_proof = mkApp (delayed_force well_founded, [| argtyp ; wf_rel |]) in
-  let argid' = id_of_string (string_of_id argname ^ "'") in
+  let argid' = Id.of_string (Id.to_string argname ^ "'") in
   let wfarg len = (Name argid', None,
   		   mkSubset (Name argid') argtyp
 		    (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
@@ -654,7 +654,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     let arg = mkApp ((delayed_force build_sigma).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
     let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
     let rcurry = mkApp (rel, [| measure; lift len measure |]) in
-    let lam = (Name (id_of_string "recproof"), None, rcurry) in
+    let lam = (Name (Id.of_string "recproof"), None, rcurry) in
     let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
     let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
       (Name recname, Some body, ty)
@@ -667,8 +667,8 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       Constrintern.compute_internalization_data env
 	Constrintern.Recursive full_arity impls 
     in
-    let newimpls = Idmap.singleton recname
-      (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))],
+    let newimpls = Id.Map.singleton recname
+      (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
        scopes @ [None]) in
       interp_casted_constr_evars isevars ~impls:newimpls
 	(push_rel_context ctx env) body (lift 1 top_arity)
@@ -759,7 +759,7 @@ let interp_recursive isfix fixl notations =
     Metasyntax.with_syntax_protection (fun () ->
       List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
       List.map4
-	(fun fixctximpenv -> interp_fix_body evdref env_rec (Idmap.fold Idmap.add fixctximpenv impls))
+	(fun fixctximpenv -> interp_fix_body evdref env_rec (Id.Map.fold Id.Map.add fixctximpenv impls))
 	fixctximpenvs fixctxs fixl fixccls)
       () in
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 47e6f5a25..a9898329a 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -35,10 +35,10 @@ val interp_definition :
   local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> definition_entry * Evd.evar_map * Impargs.manual_implicits
 
-val declare_definition : identifier -> definition_kind ->
+val declare_definition : Id.t -> definition_kind ->
   definition_entry -> Impargs.manual_implicits -> 'a declaration_hook -> 'a
 
-val do_definition : identifier -> definition_kind ->
+val do_definition : Id.t -> definition_kind ->
   local_binder list -> red_expr option -> constr_expr ->
   constr_expr option -> unit declaration_hook -> unit
 
@@ -63,9 +63,9 @@ val declare_assumptions : variable Loc.located list ->
    inductive declarations *)
 
 type structured_one_inductive_expr = {
-  ind_name : identifier;
+  ind_name : Id.t;
   ind_arity : constr_expr;
-  ind_lc : (identifier * constr_expr) list
+  ind_lc : (Id.t * constr_expr) list
 }
 
 type structured_inductive_expr =
@@ -100,8 +100,8 @@ val do_mutual_inductive :
 (** {6 Fixpoints and cofixpoints} *)
 
 type structured_fixpoint_expr = {
-  fix_name : identifier;
-  fix_annot : identifier Loc.located option;
+  fix_name : Id.t;
+  fix_annot : Id.t Loc.located option;
   fix_binders : local_binder list;
   fix_body : constr_expr option;
   fix_type : constr_expr
@@ -121,7 +121,7 @@ val extract_cofixpoint_components :
 (** Typing global fixpoints and cofixpoint_expr *)
 
 type recursive_preentry =
-  identifier list * constr option list * types list
+  Id.t list * constr option list * types list
 
 val interp_fixpoint :
   structured_fixpoint_expr list -> decl_notation list ->
@@ -151,7 +151,7 @@ val do_cofixpoint :
 
 (** Utils *)
 
-val check_mutuality : Environ.env -> bool -> (identifier * types) list -> unit
+val check_mutuality : Environ.env -> bool -> (Id.t * types) list -> unit
 
-val declare_fix : definition_object_kind -> identifier ->
+val declare_fix : definition_object_kind -> Id.t ->
   constr -> types -> Impargs.manual_implicits -> global_reference
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 1f4082b84..e40e46e69 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -56,7 +56,7 @@ let load_rcfile() =
 
 (* Puts dir in the path of ML and in the LoadPath *)
 let coq_add_path unix_path s =
-  Mltop.add_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root;Names.id_of_string s])
+  Mltop.add_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root;Names.Id.of_string s])
 let coq_add_rec_path unix_path = Mltop.add_rec_path ~unix_path ~coq_root:(Names.make_dirpath [Nameops.coq_root])
 
 (* By the option -include -I or -R of the command line *)
@@ -104,7 +104,7 @@ let init_load_path () =
     if Coq_config.local then coq_add_path (coqlib/"dev") "dev";
     (* then standard library *)
     List.iter
-      (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.id_of_string alias; Nameops.coq_root]))
+      (fun (s,alias) -> Mltop.add_rec_path ~unix_path:(coqlib/s) ~coq_root:(Names.make_dirpath [Names.Id.of_string alias; Nameops.coq_root]))
       theories_dirs_map;
     (* then plugins *)
     List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 00875a681..90652d348 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -52,7 +52,7 @@ let engage () =
 
 let set_batch_mode () = batch_mode := true
 
-let toplevel_default_name = make_dirpath [id_of_string "Top"]
+let toplevel_default_name = make_dirpath [Id.of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
 let set_toplevel_name dir =
   if dir_path_eq dir empty_dirpath then error "Need a non empty toplevel module name";
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 2f2040199..ef510aee5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -349,7 +349,7 @@ let explain_evar_kind env evi = function
       let id = Option.get ido in
       str "the implicit parameter " ++
       pr_id id ++ spc () ++ str "of" ++
-      spc () ++ Nametab.pr_global_env Idset.empty c
+      spc () ++ Nametab.pr_global_env Id.Set.empty c
   | Evar_kinds.InternalHole ->
       str "an internal placeholder" ++
 	Option.cata (fun evi ->
@@ -543,7 +543,7 @@ let explain_not_match_error = function
   | ModuleTypeFieldExpected ->
     strbrk "a module type is expected"
   | NotConvertibleInductiveField id | NotConvertibleConstructorField id ->
-    str "types given to " ++ str (string_of_id id) ++ str " differ"
+    str "types given to " ++ str (Id.to_string id) ++ str " differ"
   | NotConvertibleBodyField ->
     str "the body of definitions differs"
   | NotConvertibleTypeField ->
@@ -565,7 +565,7 @@ let explain_not_match_error = function
   | RecordProjectionsExpected nal ->
     (if List.length nal >= 2 then str "expected projection names are "
      else str "expected projection name is ") ++
-    pr_enum (function Name id -> str (string_of_id id) | _ -> str "_") nal
+    pr_enum (function Name id -> str (Id.to_string id) | _ -> str "_") nal
   | NotEqualInductiveAliases ->
     str "Aliases to inductive types do not match"
   | NoTypeConstraintExpected ->
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 5c32bd0ed..4f5bb148d 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -121,7 +121,7 @@ let interp (raw,verbosely,s) =
 (** Goal display *)
 
 let hyp_next_tac sigma env (id,_,ast) =
-  let id_s = Names.string_of_id id in
+  let id_s = Names.Id.to_string id in
   let type_s = string_of_ppcmds (pr_ltype_env env ast) in
   [
     ("clear "^id_s),("clear "^id_s^".");
@@ -230,15 +230,15 @@ let status () =
       and display the other parts (opened sections and modules) *)
   let path =
     let l = Names.repr_dirpath (Lib.cwd ()) in
-    List.rev_map Names.string_of_id l
+    List.rev_map Names.Id.to_string l
   in
   let proof =
-    try Some (Names.string_of_id (Proof_global.get_current_proof_name ()))
+    try Some (Names.Id.to_string (Proof_global.get_current_proof_name ()))
     with _ -> None
   in
   let allproofs =
     let l = Proof_global.get_all_proof_names () in
-    List.map Names.string_of_id l
+    List.map Names.Id.to_string l
   in
   {
     Interface.status_path = path;
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 722a1a748..f039a6c40 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -87,7 +87,7 @@ let scheme_object_table =
   (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t)
 
 let declare_scheme_object s aux f =
-  (try check_ident ("ind"^s) with _ ->
+  (try Id.check ("ind"^s) with _ ->
     error ("Illegal induction scheme suffix: "^s));
   let key = if String.is_empty aux then s else aux in
   try
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 7032eb46e..35ceef86a 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -41,10 +41,10 @@ val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
 
 val define_individual_scheme : individual scheme_kind -> 
   Declare.internal_flag (** internal *) ->
-  identifier option -> inductive -> constant
+  Id.t option -> inductive -> constant
 
 val define_mutual_scheme : mutual scheme_kind -> Declare.internal_flag (** internal *) ->
-  (int * identifier) list -> mutual_inductive -> constant array
+  (int * Id.t) list -> mutual_inductive -> constant array
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
 val find_scheme : 'a scheme_kind -> inductive -> constant
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index ecadc3a18..be49f41e5 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -37,17 +37,17 @@ val declare_rewriting_schemes : inductive -> unit
 (** Mutual Minimality/Induction scheme *)
 
 val do_mutual_induction_scheme :
-  (identifier located * bool * inductive * glob_sort) list -> unit
+  (Id.t located * bool * inductive * glob_sort) list -> unit
 
 (** Main calls to interpret the Scheme command *)
 
-val do_scheme : (identifier located option * scheme) list -> unit
+val do_scheme : (Id.t located option * scheme) list -> unit
 
 (** Combine a list of schemes into a conjunction of them *)
 
 val build_combined_scheme : env -> constant list -> constr * types
 
-val do_combined_scheme : identifier located -> identifier located list -> unit
+val do_combined_scheme : Id.t located -> Id.t located list -> unit
 
 (** Hook called at each inductive type definition *)
 
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index ecd1cc59b..eea41c152 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -177,7 +177,7 @@ let save id const do_guard (locality,kind) hook =
   definition_message id;
   hook l r
 
-let default_thm_id = id_of_string "Unnamed_thm"
+let default_thm_id = Id.of_string "Unnamed_thm"
 
 let compute_proof_name locality = function
   | Some (loc,id) ->
@@ -236,7 +236,7 @@ let save_named opacity =
   save id const do_guard persistence hook
 
 let check_anonymity id save_ident =
-  if not (String.equal (atompart_of_id id) (string_of_id (default_thm_id))) then
+  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
     error "This command can only be used for unnamed theorem."
 
 let save_anonymous opacity save_ident =
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index a956916f8..3c7000cb0 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.mli
@@ -18,7 +18,7 @@ open Pfedit
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (types -> unit) -> unit
 
-val start_proof : identifier -> goal_kind -> types ->
+val start_proof : Id.t -> goal_kind -> types ->
   ?init_tac:tactic -> ?compute_guard:lemma_possible_guards -> 
    unit declaration_hook -> unit
 
@@ -28,7 +28,7 @@ val start_proof_com : goal_kind ->
 
 val start_proof_with_initialization : 
   goal_kind -> (bool * lemma_possible_guards * tactic list option) option ->
-  (identifier * (types * (name list * Impargs.manual_explicitation list))) list
+  (Id.t * (types * (name list * Impargs.manual_explicitation list))) list
   -> int list option -> unit declaration_hook -> unit
 
 (** A hook the next three functions pass to cook_proof *)
@@ -44,13 +44,13 @@ val save_named : bool -> unit
 (** [save_anonymous b name] behaves as [save_named] but declares the theorem
 under the name [name] and respects the strength of the declaration *)
 
-val save_anonymous : bool -> identifier -> unit
+val save_anonymous : bool -> Id.t -> unit
 
 (** [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
    declares the theorem under the name [name] and gives it the
    strength [strength] *)
 
-val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
+val save_anonymous_with_strength : theorem_kind -> bool -> Id.t -> unit
 
 (** [admit ()] aborts the current goal and save it as an assmumption *)
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 71305cb13..f9721e2d8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -324,7 +324,7 @@ let rec find_pattern nt xl = function
 
 let rec interp_list_parser hd = function
   | [] -> [], List.rev hd
-  | NonTerminal id :: tl when id_eq id ldots_var ->
+  | NonTerminal id :: tl when Id.equal id ldots_var ->
       let hd = List.rev hd in
       let ((x,y,sl),tl') = find_pattern (List.hd hd) [] (List.tl hd,tl) in
       let xyl,tl'' = interp_list_parser [] tl' in
@@ -357,7 +357,7 @@ let rec raw_analyze_notation_tokens = function
   | String ".." :: sl -> NonTerminal ldots_var :: raw_analyze_notation_tokens sl
   | String "_" :: _ -> error "_ must be quoted."
   | String x :: sl when Lexer.is_ident x ->
-      NonTerminal (Names.id_of_string x) :: raw_analyze_notation_tokens sl
+      NonTerminal (Names.Id.of_string x) :: raw_analyze_notation_tokens sl
   | String s :: sl ->
       Terminal (String.drop_simple_quotes s) :: raw_analyze_notation_tokens sl
   | WhiteSpace n :: sl ->
@@ -374,9 +374,9 @@ let rec get_notation_vars = function
   | [] -> []
   | NonTerminal id :: sl ->
       let vars = get_notation_vars sl in
-      if id_eq id ldots_var then vars else
+      if Id.equal id ldots_var then vars else
 	if List.mem id vars then
-	  error ("Variable "^string_of_id id^" occurs more than once.")
+	  error ("Variable "^Id.to_string id^" occurs more than once.")
 	else
           id::vars
   | (Terminal _ | Break _) :: sl -> get_notation_vars sl
@@ -389,7 +389,7 @@ let analyze_notation_tokens l =
   recvars, List.subtract vars (List.map snd recvars), l
 
 let error_not_same_scope x y =
-  error ("Variables "^string_of_id x^" and "^string_of_id y^
+  error ("Variables "^Id.to_string x^" and "^Id.to_string y^
     " must be in the same scope.")
 
 (**********************************************************************)
@@ -557,7 +557,7 @@ let make_hunks etyps symbols from =
 let error_format () = error "The format does not match the notation."
 
 let rec split_format_at_ldots hd = function
-  | UnpTerminal s :: fmt when String.equal s (string_of_id ldots_var) -> List.rev hd, fmt
+  | UnpTerminal s :: fmt when String.equal s (Id.to_string ldots_var) -> List.rev hd, fmt
   | u :: fmt ->
       check_no_ldots_in_box u;
       split_format_at_ldots (u::hd) fmt
@@ -597,7 +597,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
   | Terminal s :: symbs, (UnpTerminal s') :: fmt
       when String.equal s (String.drop_simple_quotes s') ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
-  | NonTerminal s :: symbs, UnpTerminal s' :: fmt when id_eq s (id_of_string s') ->
+  | NonTerminal s :: symbs, UnpTerminal s' :: fmt when Id.equal s (Id.of_string s') ->
       let i = List.index s vars in
       let _,prec = precedence_of_entry_type from (List.nth typs (i-1)) in
       let symbs, l = aux (symbs,fmt) in symbs, UnpMetaVar (i,prec) :: l
@@ -800,14 +800,14 @@ let interp_modifiers modl =
     | [] ->
 	(assoc,level,etyps,!onlyparsing,format)
     | SetEntryType (s,typ) :: l ->
-	let id = id_of_string s in
+	let id = Id.of_string s in
 	if List.mem_assoc id etyps then
 	  error (s^" is already assigned to an entry or constr level.");
 	interp assoc level ((id,typ)::etyps) format l
     | SetItemLevel ([],n) :: l ->
 	interp assoc level etyps format l
     | SetItemLevel (s::idl,n) :: l ->
-	let id = id_of_string s in
+	let id = Id.of_string s in
 	if List.mem_assoc id etyps then
 	  error (s^" is already assigned to an entry or constr level.");
 	let typ = ETConstr (n,()) in
@@ -1239,7 +1239,7 @@ let add_notation local c ((loc,df),modifiers) sc =
 
 (* Infix notations *)
 
-let inject_var x = CRef (Ident (Loc.ghost, id_of_string x))
+let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x))
 
 let add_infix local ((loc,inf),modifiers) pr sc =
   check_infix_modifiers modifiers;
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index c7e1be39d..93752b3bc 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntax_extension :
 
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
-val add_syntactic_definition : identifier -> identifier list * constr_expr ->
+val add_syntactic_definition : Id.t -> Id.t list * constr_expr ->
   bool -> Flags.compat_version option -> unit
 
 (** Print the Camlp4 state of a grammar *)
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index 947b02924..75a0a8964 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -155,7 +155,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
     msg_warning (str ("Cannot open " ^ dir))
 
 let convert_string d =
-  try Names.id_of_string d
+  try Names.Id.of_string d
   with _ ->
     if_warn msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
     raise Exit
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 4abcfacf9..e9f31bbca 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -46,7 +46,7 @@ let check_evars env evm =
   (Evd.undefined_list evm)
 
 type oblinfo =
-  { ev_name: int * identifier;
+  { ev_name: int * Id.t;
     ev_hyps: named_context;
     ev_status: Evar_kinds.obligation_definition_status;
     ev_chop: int option;
@@ -64,7 +64,7 @@ let evar_tactic = Store.field ()
 
 let subst_evar_constr evs n idf t = 
   let seen = ref Int.Set.empty in
-  let transparent = ref Idset.empty in
+  let transparent = ref Id.Set.empty in
   let evar_info id = List.assoc id evs in
   let rec substrec (depth, fixrels) c = match kind_of_term c with
     | Evar (k, args) ->
@@ -95,7 +95,7 @@ let subst_evar_constr evs n idf t =
 	  in aux hyps args []
 	in
 	  if List.exists (fun x -> match kind_of_term x with Rel n -> List.mem n fixrels | _ -> false) args then
-	    transparent := Idset.add idstr !transparent;
+	    transparent := Id.Set.add idstr !transparent;
 	  mkApp (idf idstr, Array.of_list args)
     | Fix _ ->
 	map_constr_with_binders succfix substrec (depth, 1 :: fixrels) c
@@ -126,14 +126,14 @@ let etype_of_evar evs hyps concl =
 	let t'' = subst_vars acc 0 t' in
 	let rest, s', trans' = aux (id :: acc) (succ n) tl in
 	let s' = Int.Set.union s s' in
-	let trans' = Idset.union trans trans' in
+	let trans' = Id.Set.union trans trans' in
 	  (match copt with
 	      Some c -> 
 		let c', s'', trans'' = subst_evar_constr evs n mkVar c in
 		let c' = subst_vars acc 0 c' in
 		  mkNamedProd_or_LetIn (id, Some c', t'') rest,
 		Int.Set.union s'' s',
-		Idset.union trans'' trans'
+		Id.Set.union trans'' trans'
 	    | None ->
 		mkNamedProd_or_LetIn (id, None, t'') rest, s', trans')
     | [] ->
@@ -214,8 +214,8 @@ let eterm_obligations env name evm fs ?status t ty =
   let evn =
     let i = ref (-1) in
       List.rev_map (fun (id, ev) -> incr i;
-		      (id, (!i, id_of_string
-			      (string_of_id name ^ "_obligation_" ^ string_of_int (succ !i))),
+		      (id, (!i, Id.of_string
+			      (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))),
 		       ev)) evl
   in
   let evts =
@@ -263,7 +263,7 @@ let eterm_obligations env name evm fs ?status t ty =
 	    ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
       in
       let status = match status with
-	| Evar_kinds.Define true when Idset.mem name transparent ->
+	| Evar_kinds.Define true when Id.Set.mem name transparent ->
 	  Evar_kinds.Define false
 	| _ -> status
       in name, typ, src, status, deps, tac) evts
@@ -284,18 +284,18 @@ let error s = pperror (str s)
 let reduce c =
   Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c
 
-exception NoObligations of identifier option
+exception NoObligations of Id.t option
 
 let explain_no_obligations = function
-    Some ident -> str "No obligations for program " ++ str (string_of_id ident)
+    Some ident -> str "No obligations for program " ++ str (Id.to_string ident)
   | None -> str "No obligations remaining"
 
 type obligation_info =
-    (Names.identifier * Term.types * Evar_kinds.t Loc.located *
+    (Names.Id.t * Term.types * Evar_kinds.t Loc.located *
      Evar_kinds.obligation_definition_status * Int.Set.t * tactic option) array
 
 type obligation =
-  { obl_name : identifier;
+  { obl_name : Id.t;
     obl_type : types;
     obl_location : Evar_kinds.t Loc.located;
     obl_body : constr option;
@@ -307,17 +307,17 @@ type obligation =
 type obligations = (obligation array * int)
 
 type fixpoint_kind =
-  | IsFixpoint of (identifier Loc.located option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
 type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type program_info = {
-  prg_name: identifier;
+  prg_name: Id.t;
   prg_body: constr;
   prg_type: constr;
   prg_obligations: obligations;
-  prg_deps : identifier list;
+  prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
   prg_implicits : (Constrexpr.explicitation * (bool * bool * bool)) list;
   prg_notations : notations ;
@@ -428,7 +428,7 @@ let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
     { obl with obl_type = t' }
 
-module ProgMap = Map.Make(struct type t = identifier let compare = id_ord end)
+module ProgMap = Map.Make(struct type t = Id.t let compare = Id.compare end)
 
 let map_replace k v m = ProgMap.add k v (ProgMap.remove k m)
 
@@ -518,7 +518,7 @@ open Pp
 
 let rec lam_index n t acc =
   match kind_of_term t with
-    | Lambda (Name n', _, _) when id_eq n n' ->
+    | Lambda (Name n', _, _) when Id.equal n n' ->
       acc
     | Lambda (_, _, b) ->
 	lam_index n b (succ acc)
@@ -592,7 +592,7 @@ let declare_obligation prg obl body =
 	(DefinitionEntry ce,IsProof Property)
       in
 	if not opaque then
-	  Auto.add_hints false [string_of_id prg.prg_name]
+	  Auto.add_hints false [Id.to_string prg.prg_name]
 	    (Auto.HintsUnfoldEntry [EvalConstRef constant]);
 	definition_message obl.obl_name;
 	{ obl with obl_body = Some (mkConst constant) }
@@ -723,7 +723,7 @@ let rec string_of_list sep f = function
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
 let solve_by_tac evi t =
-  let id = id_of_string "H" in
+  let id = Id.of_string "H" in
   try
     Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
     (fun _ _ -> ());
@@ -762,7 +762,7 @@ let rec solve_obligation prg num tac =
 			else Globnames.constr_of_global gr
 		  in
 		    if transparent then
-		      Auto.add_hints true [string_of_id prg.prg_name]
+		      Auto.add_hints true [Id.to_string prg.prg_name]
 			(Auto.HintsUnfoldEntry [EvalConstRef cst]);
 		    { obl with obl_body = Some body }
 		in
@@ -873,7 +873,7 @@ let show_obligations_of_prg ?(msg=true) prg =
 		       if !showed > 0 then (
 			 decr showed;
 			 msg_info (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++
-				   str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++
+				   str "of" ++ spc() ++ str (Id.to_string n) ++ str ":" ++ spc () ++
 				   hov 1 (Printer.pr_constr_env (Global.env ()) x.obl_type ++ 
 					    str "." ++ fnl ())))
 		   | Some _ -> ())
@@ -890,13 +890,13 @@ let show_obligations ?(msg=true) n =
 let show_term n =
   let prg = get_prog_err n in
   let n = prg.prg_name in
-    (str (string_of_id n) ++ spc () ++ str":" ++ spc () ++
+    (str (Id.to_string n) ++ spc () ++ str":" ++ spc () ++
 	     Printer.pr_constr_env (Global.env ()) prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) prg.prg_body)
 
 let add_definition n ?term t ?(implicits=[]) ?(kind=Global,Definition) ?tactic
     ?(reduce=reduce) ?(hook=fun _ _ -> ()) obls =
-  let info = str (string_of_id n) ++ str " has type-checked" in
+  let info = str (Id.to_string n) ++ str " has type-checked" in
   let prg = init_prog_info n term t [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 3017db4a6..428d7e321 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -21,11 +21,11 @@ open Decl_kinds
 open Tacexpr
 
 (** Forward declaration. *)
-val declare_fix_ref : (definition_object_kind -> identifier ->
+val declare_fix_ref : (definition_object_kind -> Id.t ->
   constr -> types -> Impargs.manual_implicits -> global_reference) ref
 
 val declare_definition_ref :
-  (identifier -> locality * definition_object_kind ->
+  (Id.t -> locality * definition_object_kind ->
      Entries.definition_entry -> Impargs.manual_implicits
        -> global_reference declaration_hook -> global_reference) ref
 
@@ -38,21 +38,21 @@ val sort_dependencies : (int * evar_info * Int.Set.t) list -> (int * evar_info *
 
 (* env, id, evars, number of function prototypes to try to clear from
    evars contexts, object and type *)
-val eterm_obligations : env -> identifier -> evar_map -> int ->
+val eterm_obligations : env -> Id.t -> evar_map -> int ->
   ?status:Evar_kinds.obligation_definition_status -> constr -> types ->
-  (identifier * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Int.Set.t *
+  (Id.t * types * Evar_kinds.t Loc.located * Evar_kinds.obligation_definition_status * Int.Set.t *
       tactic option) array
     (* Existential key, obl. name, type as product, 
        location of the original evar, associated tactic,
        status and dependencies as indexes into the array *)
-  * ((existential_key * identifier) list * ((identifier -> constr) -> constr -> constr)) *
+  * ((existential_key * Id.t) list * ((Id.t -> constr) -> constr -> constr)) *
     constr * types
     (* Translations from existential identifiers to obligation identifiers 
        and for terms with existentials to closed terms, given a 
        translation from obligation identifiers to constrs, new term, new type *)
 
 type obligation_info =
-  (identifier * Term.types * Evar_kinds.t Loc.located *
+  (Id.t * Term.types * Evar_kinds.t Loc.located *
       Evar_kinds.obligation_definition_status * Int.Set.t * tactic option) array
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
@@ -69,7 +69,7 @@ val print_default_tactic : unit -> Pp.std_ppcmds
 val set_proofs_transparency : bool -> unit (* true = All transparent, false = Opaque if possible *)
 val get_proofs_transparency : unit -> bool
 
-val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> 
+val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
@@ -80,11 +80,11 @@ type notations =
     (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
 
 type fixpoint_kind =
-  | IsFixpoint of (identifier Loc.located option * Constrexpr.recursion_order_expr) list
+  | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list
   | IsCoFixpoint
 
 val add_mutual_definitions :
-  (Names.identifier * Term.constr * Term.types *
+  (Names.Id.t * Term.constr * Term.types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
@@ -93,28 +93,28 @@ val add_mutual_definitions :
   notations ->
   fixpoint_kind -> unit
 
-val obligation : int * Names.identifier option * Constrexpr.constr_expr option ->
+val obligation : int * Names.Id.t option * Constrexpr.constr_expr option ->
   Tacexpr.raw_tactic_expr option -> unit
 
-val next_obligation : Names.identifier option -> Tacexpr.raw_tactic_expr option -> unit
+val next_obligation : Names.Id.t option -> Tacexpr.raw_tactic_expr option -> unit
 
-val solve_obligations : Names.identifier option -> Proof_type.tactic option -> progress
+val solve_obligations : Names.Id.t option -> Proof_type.tactic option -> progress
 (* Number of remaining obligations to be solved for this program *)
 
 val solve_all_obligations : Proof_type.tactic option -> unit
 
-val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic option -> unit
+val try_solve_obligation : int -> Names.Id.t option -> Proof_type.tactic option -> unit
 
-val try_solve_obligations : Names.identifier option -> Proof_type.tactic option -> unit
+val try_solve_obligations : Names.Id.t option -> Proof_type.tactic option -> unit
 
-val show_obligations : ?msg:bool -> Names.identifier option -> unit
+val show_obligations : ?msg:bool -> Names.Id.t option -> unit
 
-val show_term : Names.identifier option -> std_ppcmds
+val show_term : Names.Id.t option -> std_ppcmds
 
-val admit_obligations : Names.identifier option -> unit
+val admit_obligations : Names.Id.t option -> unit
 
-exception NoObligations of Names.identifier option
+exception NoObligations of Names.Id.t option
 
-val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds
+val explain_no_obligations : Names.Id.t option -> Pp.std_ppcmds
 
 val set_program_mode : bool -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 27f63d2f8..12b87b67a 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -38,7 +38,7 @@ let interp_fields_evars evars env impls_env nots l =
       let impls =
 	match i with
 	| Anonymous -> impls
-	| Name id -> Idmap.add id (compute_internalization_data env Constrintern.Method t' impl) impls
+	| Name id -> Id.Map.add id (compute_internalization_data env Constrintern.Method t' impl) impls
       in
       let d = (i,b',t') in
       List.iter (Metasyntax.set_notation_for_interpretation impls) no;
@@ -90,14 +90,14 @@ let degenerate_decl (na,b,t) =
     | Some b -> (id, Entries.LocalDef b)
 
 type record_error =
-  | MissingProj of identifier * identifier list
-  | BadTypedProj of identifier * env * Type_errors.type_error
+  | MissingProj of Id.t * Id.t list
+  | BadTypedProj of Id.t * env * Type_errors.type_error
 
 let warning_or_error coe indsp err =
   let st = match err with
     | MissingProj (fi,projs) ->
 	let s,have = if List.length projs > 1 then "s","were" else "","was" in
-        (str(string_of_id fi) ++
+        (str(Id.to_string fi) ++
 	   strbrk" cannot be defined because the projection" ++ str s ++ spc () ++
            prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++
 	   strbrk " not defined.")
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 04691f920..e7e3330b8 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -19,15 +19,15 @@ open Globnames
    as coercions accordingly to [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
   coercion_flag list -> manual_explicitation list list -> rel_context ->
   (name * bool) list * constant option list
 
 val declare_structure : Decl_kinds.recursivity_kind ->
-  bool (**infer?*) -> identifier -> identifier ->
+  bool (**infer?*) -> Id.t -> Id.t ->
   manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
   Impargs.manual_explicitation list list -> rel_context -> (** fields *)
-  ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
+  ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
   bool -> (** coercion? *)
   bool list -> (** field coercions *)
   Evd.evar_map ->
@@ -36,4 +36,4 @@ val declare_structure : Decl_kinds.recursivity_kind ->
 val definition_structure :
   inductive_kind * Decl_kinds.recursivity_kind * bool(**infer?*)* lident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
-  identifier * constr_expr option -> global_reference
+  Id.t * constr_expr option -> global_reference
diff --git a/toplevel/search.ml b/toplevel/search.ml
index ab3b9b728..b91b96d59 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -128,7 +128,7 @@ let filter_by_module (module_list:dir_path list) (accept:bool)
     in
     xor accept (filter_aux module_list)
 
-let ref_eq = Globnames.encode_mind Coqlib.logic_module (id_of_string "eq"), 0
+let ref_eq = Globnames.encode_mind Coqlib.logic_module (Id.of_string "eq"), 0
 let c_eq = mkInd ref_eq
 let gref_eq = IndRef ref_eq
 
@@ -155,7 +155,7 @@ let filtered_search filter_function display_function ref =
 let rec id_from_pattern = function
   | PRef gr -> gr
 (* should be appear as a PRef (VarRef sp) !!
-  | PVar id -> Nametab.locate (make_qualid [] (string_of_id id))
+  | PVar id -> Nametab.locate (make_qualid [] (Id.to_string id))
  *)
   | PApp (p,_) -> id_from_pattern p
   | _ -> error "The pattern is not simple enough."
@@ -177,11 +177,11 @@ let raw_search_rewrite extra_filter display_function pattern =
 let raw_search_by_head extra_filter display_function pattern =
   Errors.todo "raw_search_by_head"
 
-let name_of_reference ref = string_of_id (basename_of_global ref)
+let name_of_reference ref = Id.to_string (basename_of_global ref)
 
 let full_name_of_reference ref =
   let (dir,id) = repr_path (path_of_global ref) in
-  string_of_dirpath dir ^ "." ^ string_of_id id
+  string_of_dirpath dir ^ "." ^ Id.to_string id
 
 (*
  * functions to use the new Libtypes facility
@@ -293,7 +293,7 @@ let interface_search flags =
     extract_flags [] [] [] [] false flags
   in
   let filter_function ref env constr =
-    let id = Names.string_of_id (Nametab.basename_of_global ref) in
+    let id = Names.Id.to_string (Nametab.basename_of_global ref) in
     let path = Libnames.dirpath (Nametab.path_of_global ref) in
     let toggle x b = if x then b else not b in
     let match_name (regexp, flag) =
@@ -319,20 +319,20 @@ let interface_search flags =
   let ans = ref [] in
   let print_function ref env constr =
     let fullpath = repr_dirpath (Nametab.dirpath_of_global ref) in
-    let qualid = Nametab.shortest_qualid_of_global Idset.empty ref in
+    let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
     let (shortpath, basename) = Libnames.repr_qualid qualid in
     let shortpath = repr_dirpath shortpath in
     (* [shortpath] is a suffix of [fullpath] and we're looking for the missing
        prefix *)
     let rec prefix full short accu = match full, short with
     | _, [] ->
-      let full = List.rev_map string_of_id full in
+      let full = List.rev_map Id.to_string full in
       (full, accu)
     | _ :: full, m :: short ->
-      prefix full short (string_of_id m :: accu)
+      prefix full short (Id.to_string m :: accu)
     | _ -> assert false
     in
-    let (prefix, qualid) = prefix fullpath shortpath [string_of_id basename] in
+    let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in
     let answer = {
       Interface.coq_object_prefix = prefix;
       Interface.coq_object_qualid = qualid;
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 435258720..0da4fc8c9 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -198,7 +198,7 @@ let valid_buffer_loc ib dloc loc =
     from cycling. *)
 let make_prompt () =
   try
-    (Names.string_of_id (Pfedit.get_current_proof_name ())) ^ " < "
+    (Names.Id.to_string (Pfedit.get_current_proof_name ())) ^ " < "
   with _ ->
     "Coq < "
 
@@ -207,7 +207,7 @@ let make_prompt () =
   let l' = ref l in
   let res =
     while List.length !l' > 1 do
-      pl := !pl ^ "|" Names.string_of_id x;
+      pl := !pl ^ "|" Names.Id.to_string x;
       l':=List.tl !l'
     done in
   let last = try List.hd !l' with _ ->   in
@@ -228,7 +228,7 @@ let make_emacs_prompt() =
   let pending = Pfedit.get_all_proof_names() in
   let pendingprompt =
     List.fold_left
-      (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.string_of_id x)
+      (fun acc x -> acc ^ (if String.is_empty acc then "" else "|") ^ Names.Id.to_string x)
       "" pending in
   let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
   if !Flags.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 71ae8a1ec..25d0fcec9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -179,9 +179,9 @@ let make_cases s =
 	       | [] -> []
 	       | (n,_)::l ->
 		   let n' = Namegen.next_name_away_in_cases_pattern n avoid in
-		   string_of_id n' :: rename (n'::avoid) l in
+		   Id.to_string n' :: rename (n'::avoid) l in
 	     let al' = rename [] al in
-	     (string_of_id consname :: al') :: l)
+	     (Id.to_string consname :: al') :: l)
 	  carr tarr []
     | _ -> raise Not_found
 
@@ -189,7 +189,7 @@ let make_cases s =
 
 let show_match id =
   let patterns =
-    try make_cases (string_of_id (snd id))
+    try make_cases (Id.to_string (snd id))
     with Not_found -> error "Unknown inductive type."
   in
   let pr_branch l =
@@ -259,7 +259,7 @@ let print_namespace ns =
         begin match match_dirpath ns dir with
         | Some [] as y -> y
         | Some (a::ns') ->
-            if Int.equal (Names.id_ord a id) 0 then Some ns'
+            if Int.equal (Names.Id.compare a id) 0 then Some ns'
             else None
         | None -> None
         end
@@ -272,7 +272,7 @@ let print_namespace ns =
         begin match match_modulepath ns mp with
         | Some [] as y -> y
         | Some (a::ns') ->
-            if Int.equal (Names.id_ord a id) 0 then Some ns'
+            if Int.equal (Names.Id.compare a id) 0 then Some ns'
             else None
         | None -> None
         end
@@ -618,7 +618,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast =
     id binders_ast (Enforce mty_ast) []
   in
     Dumpglob.dump_moddef loc mp "mod";
-    if_verbose msg_info (str ("Module "^ string_of_id id ^" is declared"));
+    if_verbose msg_info (str ("Module "^ Id.to_string id ^" is declared"));
     Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export
 
 let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
@@ -639,7 +639,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
 	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose msg_info
-	   (str ("Interactive Module "^ string_of_id id ^" started"));
+	   (str ("Interactive Module "^ Id.to_string id ^" started"));
          List.iter
            (fun (export,id) ->
              Option.iter
@@ -660,14 +660,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l =
        in
 	 Dumpglob.dump_moddef loc mp "mod";
 	 if_verbose msg_info
-	   (str ("Module "^ string_of_id id ^" is defined"));
+	   (str ("Module "^ Id.to_string id ^" is defined"));
          Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)])
            export
 
 let vernac_end_module export (loc,id as lid) =
   let mp = Declaremods.end_module () in
   Dumpglob.dump_modref loc mp "mod";
-  if_verbose msg_info (str ("Module "^ string_of_id id ^" is defined"));
+  if_verbose msg_info (str ("Module "^ Id.to_string id ^" is defined"));
   Option.iter (fun export -> vernac_import export [Ident lid]) export
 
 let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
@@ -687,7 +687,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	 Modintern.interp_modtype id binders_ast mty_sign in
         Dumpglob.dump_moddef loc mp "modtype";
 	if_verbose msg_info
-	  (str ("Interactive Module Type "^ string_of_id id ^" started"));
+	  (str ("Interactive Module Type "^ Id.to_string id ^" started"));
         List.iter
          (fun (export,id) ->
            Option.iter
@@ -707,12 +707,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l =
 	  id binders_ast mty_sign mty_ast_l in
           Dumpglob.dump_moddef loc mp "modtype";
 	  if_verbose msg_info
-	    (str ("Module Type "^ string_of_id id ^" is defined"))
+	    (str ("Module Type "^ Id.to_string id ^" is defined"))
 
 let vernac_end_modtype (loc,id) =
   let mp = Declaremods.end_modtype () in
   Dumpglob.dump_modref loc mp "modtype";
-  if_verbose msg_info (str ("Module Type "^ string_of_id id ^" is defined"))
+  if_verbose msg_info (str ("Module Type "^ Id.to_string id ^" is defined"))
 
 let vernac_include l =
   Declaremods.declare_include Modintern.interp_modexpr_or_modtype l
@@ -824,8 +824,8 @@ let vernac_set_used_variables l =
   if not (List.distinct l) then error "Used variables list contains duplicates";
   let vars = Environ.named_context (Global.env ()) in
   List.iter (fun id -> 
-    if not (List.exists (fun (id',_,_) -> id_eq id id') vars) then
-      error ("Unknown variable: " ^ string_of_id id))
+    if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then
+      error ("Unknown variable: " ^ Id.to_string id))
     l;
   set_used_variables l
 
@@ -914,7 +914,7 @@ let vernac_declare_arguments local r l nargs flags =
   let sr = smart_global r in
   let inf_names =
     Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in
-  let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in
+  let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in
   let rec check li ld ls = match li, ld, ls with
     | [], [], [] -> ()
     | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
@@ -960,10 +960,10 @@ let vernac_declare_arguments local r l nargs flags =
       let sr', impl = List.fold_map (fun b -> function
         | (Anonymous, _,_, true, max), Name id -> assert false
         | (Name x, _,_, true, _), Anonymous ->
-            error ("Argument "^string_of_id x^" cannot be declared implicit.")
+            error ("Argument "^Id.to_string x^" cannot be declared implicit.")
         | (Name iid, _,_, true, max), Name id ->
-           b || not (id_eq iid id), Some (ExplByName id, max, false)
-        | (Name iid, _,_, _, _), Name id -> b || not (id_eq iid id), None
+           b || not (Id.equal iid id), Some (ExplByName id, max, false)
+        | (Name iid, _,_, _, _), Name id -> b || not (Id.equal iid id), None
         | _ -> b, None)
         sr (List.combine il inf_names) in
       sr || sr', List.map_filter (fun x -> x) impl)
@@ -1412,7 +1412,7 @@ let interp_search_restriction = function
 
 open Search
 
-let is_ident s = try ignore (check_ident s); true with UserError _ -> false
+let is_ident s = try ignore (Id.check s); true with UserError _ -> false
 
 let interp_search_about_item = function
   | SearchSubPattern pat ->
@@ -1537,7 +1537,7 @@ let vernac_abort = function
   | Some id ->
       Backtrack.mark_unreachable [snd id];
       delete_proof id;
-      let s = string_of_id (snd id) in
+      let s = Id.to_string (snd id) in
       if_verbose msg_info (str ("Goal "^s^" aborted"))
 
 let vernac_abort_all () =
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 6aade9479..aa3cc9485 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -69,13 +69,13 @@ let rec url_list_with_sep sep f = function
   | [a] -> f a
   | a::l -> f a; url_string sep; url_list_with_sep sep f l
 
-let url_id id = url_string (string_of_id id)
+let url_id id = url_string (Id.to_string id)
 
 let uri_of_dirpath dir =
   url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir)
 
 let error_whelp_unknown_reference ref =
-  let qid = Nametab.shortest_qualid_of_global Idset.empty ref in
+  let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
   errorlabstrm ""
     (strbrk "Definitions of the current session, like " ++ pr_qualid qid ++
      strbrk ", are not supported in Whelp.")
@@ -102,7 +102,7 @@ let uri_of_ind_pointer l =
 
 let uri_of_global ref =
   match ref with
-  | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id)^".")
+  | VarRef id -> error ("Unknown Whelp reference: "^(Id.to_string id)^".")
   | ConstRef cst ->
       uri_of_repr_kn ref (repr_con cst); url_string ".con"
   | IndRef (kn,i) ->
@@ -110,7 +110,7 @@ let uri_of_global ref =
   | ConstructRef ((kn,i),j) ->
       uri_of_repr_kn ref (repr_mind kn); uri_of_ind_pointer [1;i+1;j]
 
-let whelm_special = id_of_string "WHELM_ANON_VAR"
+let whelm_special = Id.of_string "WHELM_ANON_VAR"
 
 let url_of_name = function
   | Name id -> url_id id