Modulification of identifier

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

61 files changed, 566 insertions, 573 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 2155171c9..f029c053a 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -98,7 +98,7 @@ type cinfo=
 type term=
     Symb of constr
   | Product of sorts_family * sorts_family
-  | Eps of identifier
+  | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
@@ -106,7 +106,7 @@ let rec term_equal t1 t2 =
   match t1, t2 with
     | Symb c1, Symb c2 -> eq_constr c1 c2
     | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2
-    | Eps i1, Eps i2 -> id_ord i1 i2 = 0
+    | Eps i1, Eps i2 -> Id.compare i1 i2 = 0
     | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
     | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
       Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
@@ -149,7 +149,7 @@ type patt_kind =
   | Creates_variables
 
 type quant_eq =
-    {qe_hyp_id: identifier;
+    {qe_hyp_id: Id.t;
      qe_pol: bool;
      qe_nvars:int;
      qe_lhs: ccpattern;
@@ -203,7 +203,7 @@ module Termhash = Hashtbl.Make
    end)
 
 module Identhash = Hashtbl.Make
-  (struct type t = identifier
+  (struct type t = Id.t
 	  let equal = Pervasives.(=)
 	  let hash = Hashtbl.hash
    end)
@@ -356,8 +356,8 @@ let new_representative typ =
 
 (* rebuild a constr from an applicative term *)
 
-let _A_ = Name (id_of_string "A")
-let _B_ = Name (id_of_string "A")
+let _A_ = Name (Id.of_string "A")
+let _B_ = Name (Id.of_string "A")
 let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
 
 let cc_product s1 s2 =
@@ -722,7 +722,7 @@ let one_step state =
 	    true
 	with Not_found -> false
 
-let __eps__ = id_of_string "_eps_"
+let __eps__ = Id.of_string "_eps_"
 
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 6232b126e..5d286c732 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -18,7 +18,7 @@ type cinfo =
 type term =
     Symb of constr
   | Product of sorts_family * sorts_family
-  | Eps of identifier
+  | Eps of Id.t
   | Appli of term*term
   | Constructor of cinfo (* constructor arity + nhyps *)
 
@@ -87,7 +87,7 @@ val add_equality : state -> constr -> term -> term -> unit
 
 val add_disequality : state -> from -> term -> term -> unit
 
-val add_quant : state -> identifier -> bool ->
+val add_quant : state -> Id.t -> bool ->
   int * patt_kind * ccpattern * patt_kind * ccpattern -> unit
 
 val tail_pac : pa_constructor -> pa_constructor
@@ -106,7 +106,7 @@ val join_path : forest -> int -> int ->
   ((int * int) * equality) list * ((int * int) * equality) list
 
 type quant_eq=
-    {qe_hyp_id: identifier;
+    {qe_hyp_id: Id.t;
      qe_pol: bool;
      qe_nvars:int;
      qe_lhs: ccpattern;
@@ -161,7 +161,7 @@ type term =
 
 type rule =
     Congruence
-  | Axiom of Names.identifier
+  | Axiom of Names.Id.t
   | Injection of int*int*int*int
 
 type equality =
@@ -207,19 +207,19 @@ val process_rec : UF.t -> equality list -> int list
 val cc : UF.t -> unit
 
 val make_uf :
-  (Names.identifier * (term * term)) list -> UF.t
+  (Names.Id.t * (term * term)) list -> UF.t
 
 val add_one_diseq : UF.t -> (term * term) -> int * int
 
 val add_disaxioms :
-  UF.t -> (Names.identifier * (term * term)) list ->
-  (Names.identifier * (int * int)) list
+  UF.t -> (Names.Id.t * (term * term)) list ->
+  (Names.Id.t * (int * int)) list
 
 val check_equal : UF.t -> int * int -> bool
 
 val find_contradiction : UF.t ->
-  (Names.identifier * (int * int)) list ->
-  (Names.identifier * (int * int))
+  (Names.Id.t * (int * int)) list ->
+  (Names.Id.t * (int * int))
 *)
 
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7d4d1728a..9a2f23d64 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -238,7 +238,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
   let pred=mkLambda(Anonymous,intype,outtype) in
   let case_info=make_case_info (pf_env gls) ind RegularStyle in
   let body= mkCase(case_info, pred, casee, branches) in
-  let id=pf_get_new_id (id_of_string "t") gls in
+  let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
@@ -275,7 +275,7 @@ let rec proof_tac p gls =
 	let typf = Termops.refresh_universes (pf_type_of gls tf1) in
 	let typx = Termops.refresh_universes (pf_type_of gls tx1) in
 	let typfx = Termops.refresh_universes (pf_type_of gls (mkApp (tf1,[|tx1|]))) in
-	let id = pf_get_new_id (id_of_string "f") gls in
+	let id = pf_get_new_id (Id.of_string "f") gls in
 	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 =
 	  mkApp(Lazy.force _f_equal,
@@ -316,7 +316,7 @@ let refute_tac c t1 t2 p gls =
   let neweq=
     mkApp(Lazy.force _eq,
 	  [|intype;tt1;tt2|]) in
-  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let hid=pf_get_new_id (Id.of_string "Heq") gls in
   let false_t=mkApp (c,[|mkVar hid|]) in
     tclTHENS (assert_tac (Name hid) neweq)
       [proof_tac p; simplest_elim false_t] gls
@@ -325,8 +325,8 @@ let convert_to_goal_tac c t1 t2 p gls =
   let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
   let sort = Termops.refresh_universes (pf_type_of gls tt2) in
   let neweq=mkApp(Lazy.force _eq,[|sort;tt1;tt2|]) in
-  let e=pf_get_new_id (id_of_string "e") gls in
-  let x=pf_get_new_id (id_of_string "X") gls in
+  let e=pf_get_new_id (Id.of_string "e") gls in
+  let x=pf_get_new_id (Id.of_string "X") gls in
   let identity=mkLambda (Name x,sort,mkRel 1) in
   let endt=mkApp (Lazy.force _eq_rect,
 		  [|sort;tt1;identity;c;tt2;mkVar e|]) in
@@ -335,7 +335,7 @@ let convert_to_goal_tac c t1 t2 p gls =
 
 let convert_to_hyp_tac c1 t1 c2 t2 p gls =
   let tt2=constr_of_term t2 in
-  let h=pf_get_new_id (id_of_string "H") gls in
+  let h=pf_get_new_id (Id.of_string "H") gls in
   let false_t=mkApp (c2,[|mkVar h|]) in
     tclTHENS (assert_tac (Name h) tt2)
       [convert_to_goal_tac c1 t1 t2 p;
@@ -346,13 +346,13 @@ let discriminate_tac cstr p gls =
   let intype = Termops.refresh_universes (pf_type_of gls t1) in
   let concl=pf_concl gls in
   let outsort = mkType (Termops.new_univ ()) in
-  let xid=pf_get_new_id (id_of_string "X") gls in
-  let tid=pf_get_new_id (id_of_string "t") gls in
+  let xid=pf_get_new_id (Id.of_string "X") gls in
+  let tid=pf_get_new_id (Id.of_string "t") gls in
   let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in
   let trivial=pf_type_of gls identity in
   let outtype = mkType (Termops.new_univ ()) in
   let pred=mkLambda(Name xid,outtype,mkRel 1) in
-  let hid=pf_get_new_id (id_of_string "Heq") gls in
+  let hid=pf_get_new_id (Id.of_string "Heq") gls in
   let proj=build_projection intype outtype cstr trivial concl gls in
   let injt=mkApp (Lazy.force _f_equal,
 		  [|intype;outtype;proj;t1;t2;mkVar hid|]) in
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli
index 966429682..966ebff40 100644
--- a/plugins/decl_mode/decl_expr.mli
+++ b/plugins/decl_mode/decl_expr.mli
@@ -16,7 +16,7 @@ type 'it statement =
 
 type thesis_kind =
     Plain
-  | For of identifier
+  | For of Id.t
 
 type 'this or_thesis =
     This of 'this
@@ -60,8 +60,8 @@ type ('hyp,'constr,'pat,'tac) bare_proof_instr =
   | Pconsider of 'constr*('hyp,'constr) hyp list
   | Pclaim of 'constr statement
   | Pfocus of 'constr statement
-  | Pdefine of identifier * 'hyp list * 'constr
-  | Pcast of identifier or_thesis * 'constr
+  | Pdefine of Id.t * 'hyp list * 'constr
+  | Pcast of Id.t or_thesis * 'constr
   | Psuppose of ('hyp,'constr) hyp list
   | Pcase of 'hyp list*'pat*(('hyp,'constr or_thesis) hyp list)
   | Ptake of 'constr list
@@ -77,13 +77,13 @@ type ('hyp,'constr,'pat,'tac) gen_proof_instr=
 
 
 type raw_proof_instr =
-    ((identifier*(Constrexpr.constr_expr option)) Loc.located,
+    ((Id.t*(Constrexpr.constr_expr option)) Loc.located,
      Constrexpr.constr_expr,
      Constrexpr.cases_pattern_expr,
      raw_tactic_expr) gen_proof_instr
 
 type glob_proof_instr =
-    ((identifier*(Genarg.glob_constr_and_expr option)) Loc.located,
+    ((Id.t*(Genarg.glob_constr_and_expr option)) Loc.located,
      Genarg.glob_constr_and_expr,
      Constrexpr.cases_pattern_expr,
      Tacexpr.glob_tactic_expr) gen_proof_instr
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 5e185f7e3..eb7d9e8e4 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -219,7 +219,7 @@ let interp_hyps_gen inject blend sigma env hyps head =
 
 let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop)
 
-let dummy_prefix= id_of_string "__"
+let dummy_prefix= Id.of_string "__"
 
 let rec deanonymize ids =
   function
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 1f55257e5..4bab801b1 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -24,11 +24,11 @@ let get_daimon_flag () = !daimon_flag
 open Store.Field
 
 type split_tree=
-    Skip_patt of Idset.t * split_tree
-  | Split_patt of Idset.t * inductive *
-		(bool array * (Idset.t * split_tree) option) array
+    Skip_patt of Id.Set.t * split_tree
+  | Split_patt of Id.Set.t * inductive *
+		(bool array * (Id.Set.t * split_tree) option) array
   | Close_patt of split_tree
-  | End_patt of (identifier * (int * int))
+  | End_patt of (Id.t * (int * int))
 
 type elim_kind =
     EK_dep of split_tree
@@ -48,7 +48,7 @@ type per_info =
      per_wf:recpath}
 
 type stack_info =
-    Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
+    Per of Decl_expr.elim_type * per_info * elim_kind * Id.t list
   | Suppose_case
   | Claim
   | Focus_claim
diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli
index f23a97b4e..853135f10 100644
--- a/plugins/decl_mode/decl_mode.mli
+++ b/plugins/decl_mode/decl_mode.mli
@@ -27,11 +27,11 @@ val get_current_mode : unit -> command_mode
 val check_not_proof_mode : string -> unit
 
 type split_tree=
-    Skip_patt of Idset.t * split_tree
-  | Split_patt of Idset.t * inductive *
-		(bool array * (Idset.t * split_tree) option) array
+    Skip_patt of Id.Set.t * split_tree
+  | Split_patt of Id.Set.t * inductive *
+		(bool array * (Id.Set.t * split_tree) option) array
   | Close_patt of split_tree
-  | End_patt of (identifier * (int * int))
+  | End_patt of (Id.t * (int * int))
 
 type elim_kind =
     EK_dep of split_tree
@@ -51,7 +51,7 @@ type per_info =
      per_wf:recpath}
 
 type stack_info =
-    Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
+    Per of Decl_expr.elim_type * per_info * elim_kind * Names.Id.t list
   | Suppose_case
   | Claim
   | Focus_claim
@@ -69,7 +69,7 @@ val get_stack : Proof.proof -> stack_info list
 
 val get_top_stack : Proof.proof -> stack_info list
 
-val get_last:  Environ.env -> identifier
+val get_last:  Environ.env -> Id.t
 
 val focus : Proof.proof -> unit
 
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 8075f05e9..a42e0cb3e 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -91,7 +91,7 @@ let mk_evd metalist gls =
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
 
-let is_tmp id = (string_of_id id).[0] = '_'
+let is_tmp id = (Id.to_string id).[0] = '_'
 
 let tmp_ids gls =
   let ctx = pf_hyps gls in
@@ -210,27 +210,27 @@ let filter_hyps f gls =
       tclTRY (clear [id])  in
     tclMAP filter_aux (pf_hyps gls) gls
 
-let local_hyp_prefix = id_of_string "___"
+let local_hyp_prefix = Id.of_string "___"
 
 let add_justification_hyps keep items gls =
   let add_aux c gls=
     match kind_of_term c with
 	Var id ->
-	  keep:=Idset.add id !keep;
+	  keep:=Id.Set.add id !keep;
 	  tclIDTAC gls
       | _ ->
 	  let id=pf_get_new_id local_hyp_prefix gls in
-	    keep:=Idset.add id !keep;
+	    keep:=Id.Set.add id !keep;
 	    tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere)
               (thin_body [id]) gls in
     tclMAP add_aux items gls
 
 let prepare_goal items gls =
-  let tokeep = ref Idset.empty in
+  let tokeep = ref Id.Set.empty in
   let auxres = add_justification_hyps tokeep items gls in
    tclTHENLIST
      [ (fun _ -> auxres);
-       filter_hyps (let keep = !tokeep in fun id -> Idset.mem id keep)] gls
+       filter_hyps (let keep = !tokeep in fun id -> Id.Set.mem id keep)] gls
 
 let my_automation_tac = ref
   (fun gls -> anomaly "No automation registered")
@@ -474,7 +474,7 @@ let instr_cut mkstat _thus _then cut gls0 =
   let stat = cut.cut_stat in
   let (c_id,_) = match stat.st_label with
       Anonymous ->
-	pf_get_new_id (id_of_string "_fact") gls0,false
+	pf_get_new_id (Id.of_string "_fact") gls0,false
     | Name id -> id,true in
   let c_stat = mkstat info gls0 stat.st_it in
   let thus_tac gls=
@@ -520,7 +520,7 @@ let instr_rew _thus rew_side cut gls0 =
     justification (tclTHEN items_tac method_tac) gls in
   let (c_id,_) = match cut.cut_stat.st_label with
       Anonymous ->
-	pf_get_new_id (id_of_string "_eq") gls0,false
+	pf_get_new_id (Id.of_string "_eq") gls0,false
     | Name id -> id,true in
   let thus_tac new_eq gls=
     if _thus then
@@ -549,7 +549,7 @@ let instr_rew _thus rew_side cut gls0 =
 let instr_claim _thus st gls0 =
   let info = get_its_info gls0 in
   let (id,_) = match st.st_label with
-      Anonymous -> pf_get_new_id (id_of_string "_claim") gls0,false
+      Anonymous -> pf_get_new_id (Id.of_string "_claim") gls0,false
     | Name id -> id,true in
   let thus_tac gls=
     if _thus then
@@ -566,7 +566,7 @@ let instr_claim _thus st gls0 =
 let push_intro_tac coerce nam gls =
       let (hid,_) =
 	match nam with
-	    Anonymous -> pf_get_new_id (id_of_string "_hyp") gls,false
+	    Anonymous -> pf_get_new_id (Id.of_string "_hyp") gls,false
 	  | Name id -> id,true in
 	tclTHENLIST
 	  [intro_mustbe_force hid;
@@ -640,7 +640,7 @@ let rec build_applist prod = function
 
 let instr_suffices _then cut gls0 =
   let info = get_its_info gls0 in
-  let c_id = pf_get_new_id (id_of_string "_cofact") gls0 in
+  let c_id = pf_get_new_id (Id.of_string "_cofact") gls0 in
   let ctx,hd = cut.cut_stat in
   let c_stat = build_product ctx (mk_stat_or_thesis info gls0 hd) in
   let metas = metas_from 1 ctx in
@@ -677,7 +677,7 @@ let rec intron_then n ids ltac gls =
   if n<=0 then
     ltac ids gls
   else
-    let id = pf_get_new_id (id_of_string "_tmp") gls in
+    let id = pf_get_new_id (Id.of_string "_tmp") gls in
       tclTHEN
 	(intro_mustbe_force id)
 	(intron_then (pred n) (id::ids) ltac) gls
@@ -692,7 +692,7 @@ let rec consider_match may_intro introduced available expected gls =
     | [],hyps ->
 	if may_intro then
 	  begin
- 	    let id = pf_get_new_id (id_of_string "_tmp") gls in
+ 	    let id = pf_get_new_id (Id.of_string "_tmp") gls in
 	      tclIFTHENELSE
 		(intro_mustbe_force id)
 		(consider_match true [] [id] hyps)
@@ -732,7 +732,7 @@ let consider_tac c hyps gls =
       Var id ->
 	consider_match false [] [id] hyps gls
     | _ ->
-	let id = pf_get_new_id (id_of_string "_tmp") gls in
+	let id = pf_get_new_id (Id.of_string "_tmp") gls in
 	tclTHEN
 	  (forward None (Some (Loc.ghost, IntroIdentifier id)) c)
  	  (consider_match false [] [id] hyps) gls
@@ -823,7 +823,7 @@ let map_tree id_fun mapi = function
 
 
 let start_tree env ind rp =
-  init_tree Idset.empty ind rp (fun _ _ -> None)
+  init_tree Id.Set.empty ind rp (fun _ _ -> None)
 
 let build_per_info etype casee gls =
   let concl=pf_concl gls in
@@ -872,7 +872,7 @@ let per_tac etype casee gls=
 		  Per(etype,per_info,ek,[])::info.pm_stack} gls
       | Virtual cut ->
 	  assert (cut.cut_stat.st_label=Anonymous);
-	  let id = pf_get_new_id (id_of_string "anonymous_matched") gls in
+	  let id = pf_get_new_id (Id.of_string "anonymous_matched") gls in
 	  let c = mkVar id in
 	  let modified_cut =
 	    {cut with cut_stat={cut.cut_stat with st_label=Name id}} in
@@ -901,7 +901,7 @@ let register_nodep_subcase id= function
 let suppose_tac hyps gls0 =
   let info = get_its_info gls0 in
   let thesis = pf_concl gls0 in
-  let id = pf_get_new_id (id_of_string "subcase_") gls0 in
+  let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
   let clause = build_product hyps thesis in
   let ninfo1 = {pm_stack=Suppose_case::info.pm_stack} in
   let old_clauses,stack = register_nodep_subcase id info.pm_stack in
@@ -931,17 +931,17 @@ let rec tree_of_pats ((id,_) as cpl) pats =
 	  | (patt,rp) :: rest_args ->
 	      match patt with
 		  PatVar (_,v) ->
-		    Skip_patt (Idset.singleton id,
+		    Skip_patt (Id.Set.singleton id,
 			       tree_of_pats cpl (rest_args::stack))
 		| PatCstr (_,(ind,cnum),args,nam) ->
 		    let nexti i ati =
 		      if i = pred cnum then
 			let nargs =
 			  List.map_i (fun j a -> (a,ati.(j))) 0 args in
-			  Some (Idset.singleton id,
+			  Some (Id.Set.singleton id,
 				tree_of_pats cpl (nargs::rest_args::stack))
 		      else None
-		      in init_tree Idset.empty ind rp nexti
+		      in init_tree Id.Set.empty ind rp nexti
 
 let rec add_branch ((id,_) as cpl) pats tree=
   match pats with
@@ -967,10 +967,10 @@ let rec add_branch ((id,_) as cpl) pats tree=
 		    begin
 		      match tree with
 			  Skip_patt (ids,t) ->
-			    Skip_patt (Idset.add id ids,
+			    Skip_patt (Id.Set.add id ids,
 				       add_branch cpl (rest_args::stack) t)
 			| Split_patt (_,_,_) ->
-			    map_tree (Idset.add id)
+			    map_tree (Id.Set.add id)
 			      (fun i bri ->
 				 append_branch cpl 1 (rest_args::stack) bri)
 			      tree
@@ -983,7 +983,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 			    if i = pred cnum then
 			      let nargs =
 				List.map_i (fun j a -> (a,ati.(j))) 0 args in
-				Some (Idset.add id ids,
+				Some (Id.Set.add id ids,
 				      add_branch cpl (nargs::rest_args::stack)
 					(skip_args t ids (Array.length ati)))
 			    else
@@ -1005,19 +1005,19 @@ let rec add_branch ((id,_) as cpl) pats tree=
 		      | _ -> anomaly "No pop/stop expected here"
 and append_branch ((id,_) as cpl) depth pats = function
     Some (ids,tree) ->
-      Some (Idset.add id ids,append_tree cpl depth pats tree)
+      Some (Id.Set.add id ids,append_tree cpl depth pats tree)
   | None ->
-      Some (Idset.singleton id,tree_of_pats cpl pats)
+      Some (Id.Set.singleton id,tree_of_pats cpl pats)
 and append_tree ((id,_) as cpl) depth pats tree =
   if depth<=0 then add_branch cpl pats tree
   else match tree with
       Close_patt t ->
 	Close_patt (append_tree cpl (pred depth) pats t)
     | Skip_patt (ids,t) ->
-	Skip_patt (Idset.add id ids,append_tree cpl depth pats t)
+	Skip_patt (Id.Set.add id ids,append_tree cpl depth pats t)
     | End_patt _ -> anomaly "Premature end of branch"
     | Split_patt (_,_,_) ->
-	map_tree (Idset.add id)
+	map_tree (Id.Set.add id)
 	  (fun i bri -> append_branch cpl (succ depth) pats bri) tree
 
 (* suppose it is *)
@@ -1101,7 +1101,7 @@ let rec register_dep_subcase id env per_info pat = function
 
 let case_tac params pat_info hyps gls0 =
   let info = get_its_info gls0 in
-  let id = pf_get_new_id (id_of_string "subcase_") gls0 in
+  let id = pf_get_new_id (Id.of_string "subcase_") gls0 in
   let et,per_info,ek,old_clauses,rest =
     match info.pm_stack with
 	Per (et,pi,ek,old_clauses)::rest -> (et,pi,ek,old_clauses,rest)
@@ -1139,7 +1139,7 @@ let push_arg arg stacks =
 
 
 let push_one_head c ids (id,stack) =
-  let head = if Idset.mem id ids then Some c else None in
+  let head = if Id.Set.mem id ids then Some c else None in
     id,(head,[]) :: stack
 
 let push_head c ids stacks =
@@ -1251,7 +1251,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 		 | Some (sub_ids,tree) ->
 		     let br_args =
 		       List.filter
-			 (fun (id,_) -> Idset.mem id sub_ids) args in
+			 (fun (id,_) -> Id.Set.mem id sub_ids) args in
 		     let construct =
 		       applist (mkConstruct(ind,succ i),params) in
 		     let p_args =
@@ -1333,9 +1333,9 @@ let end_tac et2 gls =
 		  begin
 		    fun gls0 ->
 		      let fix_id =
-			pf_get_new_id (id_of_string "_fix") gls0 in
+			pf_get_new_id (Id.of_string "_fix") gls0 in
 		      let c_id =
-			pf_get_new_id (id_of_string "_main_arg") gls0 in
+			pf_get_new_id (Id.of_string "_main_arg") gls0 in
 			tclTHENLIST
 			  [fix (Some fix_id) (succ nargs);
 			   tclDO nargs introf;
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 775d2f535..fb7e5c29a 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -31,24 +31,24 @@ val execute_cases :
     Names.name ->
     Decl_mode.per_info ->
     (Term.constr -> Proof_type.tactic) ->
-    (Names.Idset.elt * (Term.constr option * Term.constr list) list) list ->
+    (Names.Id.Set.elt * (Term.constr option * Term.constr list) list) list ->
     Term.constr list -> int -> Decl_mode.split_tree -> Proof_type.tactic
 
 val tree_of_pats : 
-  identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
+  Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
   split_tree
 
 val add_branch : 
-  identifier * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
+  Id.t * (int * int) -> (Glob_term.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val append_branch :
-  identifier *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
-  (Names.Idset.t * Decl_mode.split_tree) option ->
-  (Names.Idset.t * Decl_mode.split_tree) option
+  Id.t *(int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
+  (Names.Id.Set.t * Decl_mode.split_tree) option ->
+  (Names.Id.Set.t * Decl_mode.split_tree) option
 
 val append_tree :
-  identifier * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
+  Id.t * (int * int) -> int -> (Glob_term.cases_pattern*recpath) list list ->
   split_tree -> split_tree
 
 val build_dep_clause :   Term.types Decl_expr.statement list ->
@@ -58,7 +58,7 @@ val build_dep_clause :   Term.types Decl_expr.statement list ->
     Decl_expr.hyp list -> Proof_type.goal Tacmach.sigma -> Term.types
 
 val register_dep_subcase :    
-    Names.identifier * (int * int) ->
+    Names.Id.t * (int * int) ->
     Environ.env ->
     Decl_mode.per_info ->
     Glob_term.cases_pattern -> Decl_mode.elim_kind -> Decl_mode.elim_kind
@@ -69,41 +69,41 @@ val thesis_for :     Term.constr ->
 val close_previous_case : Proof.proof -> unit
 
 val pop_stacks :
-  (Names.identifier *
+  (Names.Id.t *
      (Term.constr option * Term.constr list) list) list ->
-  (Names.identifier *
+  (Names.Id.t *
      (Term.constr option * Term.constr list) list) list
 
 val push_head :   Term.constr ->
-  Names.Idset.t ->
-  (Names.identifier *
+  Names.Id.Set.t ->
+  (Names.Id.t *
      (Term.constr option * Term.constr list) list) list ->
-  (Names.identifier *
+  (Names.Id.t *
      (Term.constr option * Term.constr list) list) list
 
 val push_arg : Term.constr ->
-  (Names.identifier *
+  (Names.Id.t *
      (Term.constr option * Term.constr list) list) list ->
-  (Names.identifier *
+  (Names.Id.t *
      (Term.constr option * Term.constr list) list) list
 
 val hrec_for:
-    Names.identifier ->
+    Names.Id.t ->
     Decl_mode.per_info -> Proof_type.goal Tacmach.sigma ->
-    Names.identifier -> Term.constr
+    Names.Id.t -> Term.constr
 
 val consider_match :
    bool ->
-    (Names.Idset.elt*bool) list ->
-    Names.Idset.elt list ->
+    (Names.Id.Set.elt*bool) list ->
+    Names.Id.Set.elt list ->
     (Term.types Decl_expr.statement, Term.types) Decl_expr.hyp list ->
     Proof_type.tactic
 
 val init_tree:
-    Names.Idset.t ->
+    Names.Id.Set.t ->
     Names.inductive ->
     int option * Declarations.wf_paths ->
     (int ->
      (int option * Declarations.recarg Rtree.t) array ->
-     (Names.Idset.t * Decl_mode.split_tree) option) ->
+     (Names.Id.Set.t * Decl_mode.split_tree) option) ->
     Decl_mode.split_tree
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 04cc167a8..3269befdb 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -18,7 +18,7 @@ open Miniml
 open Mlutil
 
 let string_of_id id =
-  let s = Names.string_of_id id in
+  let s = Names.Id.to_string id in
   for i = 0 to String.length s - 2 do
     if s.[i] = '_' && s.[i+1] = '_' then warning_id s
   done;
@@ -109,12 +109,12 @@ let pseudo_qualify = qualify "__"
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
-let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id))
 let uppercase_id id =
   let s = string_of_id id in
   assert (s<>"");
-  if s.[0] = '_' then id_of_string ("Coq_"^s)
-  else id_of_string (String.capitalize s)
+  if s.[0] = '_' then Id.of_string ("Coq_"^s)
+  else Id.of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
@@ -128,12 +128,12 @@ let kindcase_id k id =
 
 (*s de Bruijn environments for programs *)
 
-type env = identifier list * Idset.t
+type env = Id.t list * Id.Set.t
 
 (*s Generic renaming issues for local variable names. *)
 
 let rec rename_id id avoid =
-  if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
+  if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id
 
 let rec rename_vars avoid = function
   | [] ->
@@ -145,14 +145,14 @@ let rec rename_vars avoid = function
   | id :: idl ->
       let (idl, avoid) = rename_vars avoid idl in
       let id = rename_id (lowercase_id id) avoid in
-      (id :: idl, Idset.add id avoid)
+      (id :: idl, Id.Set.add id avoid)
 
 let rename_tvars avoid l =
   let rec rename avoid = function
     | [] -> [],avoid
     | id :: idl ->
 	let id = rename_id (lowercase_id id) avoid in
-	let idl, avoid = rename (Idset.add id avoid) idl in
+	let idl, avoid = rename (Id.Set.add id avoid) idl in
 	(id :: idl, avoid) in
   fst (rename avoid l)
 
@@ -162,7 +162,7 @@ let push_vars ids (db,avoid) =
 
 let get_db_name n (db,_) =
   let id = List.nth db (pred n) in
-  if id = dummy_name then id_of_string "__" else id
+  if id = dummy_name then Id.of_string "__" else id
 
 
 (*S Renamings of global objects. *)
@@ -179,13 +179,13 @@ let set_phase, get_phase =
   let ph = ref Impl in ((:=) ph), (fun () -> !ph)
 
 let set_keywords, get_keywords =
-  let k = ref Idset.empty in
+  let k = ref Id.Set.empty in
   ((:=) k), (fun () -> !k)
 
 let add_global_ids, get_global_ids =
-  let ids = ref Idset.empty in
+  let ids = ref Id.Set.empty in
   register_cleanup (fun () -> ids := get_keywords ());
-  let add s = ids := Idset.add s !ids
+  let add s = ids := Id.Set.add s !ids
   and get () = !ids
   in (add,get)
 
@@ -309,7 +309,7 @@ let modular_rename k id =
     if upperkind k then "Coq_",is_upper else "coq_",is_lower
   in
   if not (is_ok s) ||
-    (Idset.mem id (get_keywords ())) ||
+    (Id.Set.mem id (get_keywords ())) ||
     (String.length s >= 4 && String.sub s 0 4 = prefix)
   then prefix ^ s
   else s
@@ -320,7 +320,7 @@ let modular_rename k id =
 let modfstlev_rename =
   let add_prefixes,get_prefixes,_ = mktable true in
   fun l ->
-    let coqid = id_of_string "Coq" in
+    let coqid = Id.of_string "Coq" in
     let id = id_of_label l in
     try
       let coqset = get_prefixes id in
@@ -372,12 +372,12 @@ let ref_renaming_fun (k,r) =
     let idg = safe_basename_of_global r in
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
-      let globs = Idset.elements (get_global_ids ()) in
+      let globs = Id.Set.elements (get_global_ids ()) in
       let id = next_ident_away (kindcase_id k idg) globs in
       string_of_id id
     else modular_rename k idg
   in
-  add_global_ids (id_of_string s);
+  add_global_ids (Id.of_string s);
   s::l
 
 (* Cached version of the last function *)
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 7233b8c2b..9ddd0f2af 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -33,17 +33,17 @@ val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds
 val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 
-val pr_binding : identifier list -> std_ppcmds
+val pr_binding : Id.t list -> std_ppcmds
 
-val rename_id : identifier -> Idset.t -> identifier
+val rename_id : Id.t -> Id.Set.t -> Id.t
 
-type env = identifier list * Idset.t
+type env = Id.t list * Id.Set.t
 val empty_env : unit -> env
 
-val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: Idset.t -> identifier list -> identifier list
-val push_vars : identifier list -> env -> identifier list * env
-val get_db_name : int -> env -> identifier
+val rename_vars: Id.Set.t -> Id.t list -> env
+val rename_tvars: Id.Set.t -> Id.t list -> Id.t list
+val push_vars : Id.t list -> env -> Id.t list * env
+val get_db_name : int -> env -> Id.t
 
 type phase = Pre | Impl | Intf
 
@@ -69,7 +69,7 @@ type reset_kind = AllButExternal | Everything
 
 val reset_renaming_tables : reset_kind -> unit
 
-val set_keywords : Idset.t -> unit
+val set_keywords : Id.Set.t -> unit
 
 (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 0b4047f17..3cd3f7f8a 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -388,7 +388,7 @@ let descr () = match lang () with
 (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
    Works similarly for the other languages. *)
 
-let default_id = id_of_string "Main"
+let default_id = Id.of_string "Main"
 
 let mono_filename f =
   let d = descr () in
@@ -402,7 +402,7 @@ let mono_filename f =
 	in
 	let id =
 	  if lang () <> Haskell then default_id
-	  else try id_of_string (Filename.basename f)
+	  else try Id.of_string (Filename.basename f)
 	  with _ -> error "Extraction: provided filename is not a valid identifier"
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
@@ -412,7 +412,7 @@ let mono_filename f =
 let module_filename mp =
   let f = file_of_modfile mp in
   let d = descr () in
-  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
+  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f
 
 (*s Extraction of one decl to stdout. *)
 
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 5e14214b9..6c648b981 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -15,7 +15,7 @@ open Globnames
 val simple_extraction : reference -> unit
 val full_extraction : string option -> reference list -> unit
 val separate_extraction : reference list -> unit
-val extraction_library : bool -> identifier -> unit
+val extraction_library : bool -> Id.t -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6645f1d5d..5b31db3f9 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -192,7 +192,7 @@ let parse_ind_args si args relmax =
   in parse 1 1 si
 
 let oib_equal o1 o2 =
-  id_ord o1.mind_typename o2.mind_typename = 0 &&
+  Id.compare o1.mind_typename o2.mind_typename = 0 &&
   List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
   begin match o1.mind_arity, o2.mind_arity with
   | Monomorphic {mind_user_arity=c1; mind_sort=s1},
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 1eb9ca8e5..3a5fc9794 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -19,7 +19,7 @@ val extract_constant : env -> constant -> constant_body -> ml_decl
 
 val extract_constant_spec : env -> constant -> constant_body -> ml_spec
 
-val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option
+val extract_with_type : env -> constant_body -> ( Id.t list * ml_type ) option
 
 val extract_fixpoint :
   env -> constant array -> (constr, types) prec_declaration -> ml_decl
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index bdb102b18..5295e2cf9 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -33,7 +33,7 @@ let pr_int_or_id _ _ _ = function
 ARGUMENT EXTEND int_or_id
   TYPED AS int_or_id
   PRINTED BY pr_int_or_id
-| [ preident(id) ] -> [ ArgId (id_of_string id) ]
+| [ preident(id) ] -> [ ArgId (Id.of_string id) ]
 | [ integer(i) ] -> [ ArgInt i ]
 END
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 5de13e53c..3925a2a2f 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,16 +21,16 @@ open Common
 
 (*s Haskell renaming issues. *)
 
-let pr_lower_id id = str (String.uncapitalize (string_of_id id))
-let pr_upper_id id = str (String.capitalize (string_of_id id))
+let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
+let pr_upper_id id = str (String.capitalize (Id.to_string id))
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
-  Idset.empty
+  Id.Set.empty
 
 let pp_comment s = str "-- " ++ s ++ fnl ()
 let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index d170acbb0..14a30ae79 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -65,11 +65,11 @@ type inductive_kind =
 *)
 
 type ml_ind_packet = {
-  ip_typename : identifier;
-  ip_consnames : identifier array;
+  ip_typename : Id.t;
+  ip_consnames : Id.t array;
   ip_logical : bool;
   ip_sign : signature;
-  ip_vars : identifier list;
+  ip_vars : Id.t list;
   ip_types : (ml_type list) array
 }
 
@@ -91,8 +91,8 @@ type ml_ind = {
 
 type ml_ident =
   | Dummy
-  | Id of identifier
-  | Tmp of identifier
+  | Id of Id.t
+  | Tmp of Id.t
 
 (** We now store some typing information on constructors
     and cases to avoid type-unsafe optimisations. This will be
@@ -116,7 +116,7 @@ and ml_ast =
   | MLcons   of ml_type * global_reference * ml_ast list
   | MLtuple  of ml_ast list
   | MLcase   of ml_type * ml_ast * ml_branch array
-  | MLfix    of int * identifier array * ml_ast array
+  | MLfix    of int * Id.t array * ml_ast array
   | MLexn    of string
   | MLdummy
   | MLaxiom
@@ -133,13 +133,13 @@ and ml_pattern =
 
 type ml_decl =
   | Dind  of mutual_inductive * ml_ind
-  | Dtype of global_reference * identifier list * ml_type
+  | Dtype of global_reference * Id.t list * ml_type
   | Dterm of global_reference * ml_ast * ml_type
   | Dfix  of global_reference array * ml_ast array * ml_type array
 
 type ml_spec =
   | Sind  of mutual_inductive * ml_ind
-  | Stype of global_reference * identifier list * ml_type option
+  | Stype of global_reference * Id.t list * ml_type option
   | Sval  of global_reference * ml_type
 
 type ml_specif =
@@ -154,8 +154,8 @@ and ml_module_type =
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
-  | ML_With_type of identifier list * identifier list * ml_type
-  | ML_With_module of identifier list * module_path
+  | ML_With_type of Id.t list * Id.t list * ml_type
+  | ML_With_module of Id.t list * module_path
 
 and ml_module_sig = (label * ml_specif) list
 
@@ -191,13 +191,13 @@ type unsafe_needs = {
 }
 
 type language_descr = {
-  keywords : Idset.t;
+  keywords : Id.Set.t;
 
   (* Concerning the source file *)
   file_suffix : string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
-    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
     std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
@@ -205,7 +205,7 @@ type language_descr = {
   sig_suffix : string option;
   (* the second argument is a comment to add to the preamble *)
   sig_preamble :
-    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
     std_ppcmds;
   pp_sig : ml_signature -> std_ppcmds;
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 18c3f840e..d8d1d1eae 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -22,8 +22,8 @@ exception Impossible
 
 (*S Names operations. *)
 
-let anonymous_name = id_of_string "x"
-let dummy_name = id_of_string "_"
+let anonymous_name = Id.of_string "x"
+let dummy_name = Id.of_string "_"
 
 let anonymous = Id anonymous_name
 
@@ -857,7 +857,7 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
 
 let is_program_branch = function
   | Id id ->
-    let s = string_of_id id in
+    let s = Id.to_string id in
     let br = "program_branch_" in
     let n = String.length br in
     (try
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index be32ba6ed..1c70908b6 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -77,10 +77,10 @@ val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
 
-val anonymous_name : identifier
-val dummy_name : identifier
-val id_of_name : name -> identifier
-val id_of_mlid : ml_ident -> identifier
+val anonymous_name : Id.t
+val dummy_name : Id.t
+val id_of_name : name -> Id.t
+val id_of_mlid : ml_ident -> Id.t
 val tmp_id : ml_ident -> ml_ident
 
 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 7640416fd..b8d75d445 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -24,7 +24,7 @@ open Common
 (*s Some utility functions. *)
 
 let pp_tvar id =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   if String.length s < 2 || s.[1]<>'\''
   then str ("'"^s)
   else str ("' "^s)
@@ -48,7 +48,7 @@ let pp_letin pat def body =
 (*s Ocaml renaming issues. *)
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
   [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
     "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
     "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
@@ -57,7 +57,7 @@ let keywords =
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
-  Idset.empty
+  Id.Set.empty
 
 let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index bfbcc7b0a..8125b4757 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -20,11 +20,11 @@ open Common
 (*s Scheme renaming issues. *)
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
     [ "define"; "let"; "lambda"; "lambdas"; "match";
       "apply"; "car"; "cdr";
       "error"; "delay"; "force"; "_"; "__"]
-    Idset.empty
+    Id.Set.empty
 
 let pp_comment s = str";; "++h 0 s++fnl ()
 
@@ -40,7 +40,7 @@ let preamble _ comment _ usf =
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   for i = 0 to String.length s - 1 do
     if s.[i] = '\'' then s.[i] <- '~'
   done;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index dd3b65b90..c7d8d42de 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -56,7 +56,7 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
+  | MPfile f -> String.capitalize (Id.to_string (List.hd (repr_dirpath f)))
   | _ -> assert false
 
 let current_toplevel () = fst (Lib.current_prefix ())
@@ -256,8 +256,8 @@ let safe_basename_of_global r =
     | VarRef _ -> assert false
 
 let string_of_global r =
- try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
- with _ -> string_of_id (safe_basename_of_global r)
+ try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r)
+ with _ -> Id.to_string (safe_basename_of_global r)
 
 let safe_pr_global r = str (string_of_global r)
 
@@ -273,7 +273,7 @@ let safe_pr_long_global r =
 
 let pr_long_mp mp =
   let lid = repr_dirpath (Nametab.dirpath_of_module mp) in
-  str (String.concat "." (List.map string_of_id (List.rev lid)))
+  str (String.concat "." (List.map Id.to_string (List.rev lid)))
 
 let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
@@ -411,7 +411,7 @@ let error_MPfile_as_mod mp b =
 let msg_non_implicit r n id =
   let name = match id with
     | Anonymous -> ""
-    | Name id -> "(" ^ string_of_id id ^ ") "
+    | Name id -> "(" ^ Id.to_string id ^ ") "
   in
   "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
 
@@ -652,7 +652,7 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extraction Implicit *)
 
-type int_or_id = ArgInt of int | ArgId of identifier
+type int_or_id = ArgInt of int | ArgId of Id.t
 
 let implicits_table = ref Refmap'.empty
 
@@ -704,21 +704,21 @@ let extraction_implicit r l =
 
 (*s Extraction Blacklist of filenames not to use while extracting *)
 
-let blacklist_table = ref Idset.empty
+let blacklist_table = ref Id.Set.empty
 
 let modfile_ids = ref []
 let modfile_mps = ref MPmap.empty
 
 let reset_modfile () =
-  modfile_ids := Idset.elements !blacklist_table;
+  modfile_ids := Id.Set.elements !blacklist_table;
   modfile_mps := MPmap.empty
 
 let string_of_modfile mp =
   try MPmap.find mp !modfile_mps
   with Not_found ->
-    let id = id_of_string (raw_string_of_modfile mp) in
+    let id = Id.of_string (raw_string_of_modfile mp) in
     let id' = next_ident_away id !modfile_ids in
-    let s' = string_of_id id' in
+    let s' = Id.to_string id' in
     modfile_ids := id' :: !modfile_ids;
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'
@@ -727,7 +727,7 @@ let string_of_modfile mp =
 
 let file_of_modfile mp =
   let s0 = match mp with
-    | MPfile f -> string_of_id (List.hd (repr_dirpath f))
+    | MPfile f -> Id.to_string (List.hd (repr_dirpath f))
     | _ -> assert false
   in
   let s = String.copy (string_of_modfile mp) in
@@ -736,7 +736,7 @@ let file_of_modfile mp =
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
+    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)
@@ -752,26 +752,26 @@ let blacklist_extraction : string list -> obj =
 let _ = declare_summary "Extraction Blacklist"
 	  { freeze_function = (fun () -> !blacklist_table);
 	    unfreeze_function = ((:=) blacklist_table);
-	    init_function = (fun () -> blacklist_table := Idset.empty) }
+	    init_function = (fun () -> blacklist_table := Id.Set.empty) }
 
 (* Grammar entries. *)
 
 let extraction_blacklist l =
-  let l = List.rev_map string_of_id l in
+  let l = List.rev_map Id.to_string l in
   Lib.add_anonymous_leaf (blacklist_extraction l)
 
 (* Printing part *)
 
 let print_extraction_blacklist () =
-  prlist_with_sep fnl pr_id (Idset.elements !blacklist_table)
+  prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table)
 
 (* Reset part *)
 
 let reset_blacklist : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
-       cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)}
+       cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty);
+       load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)}
 
 let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 16c2275f1..fbf48889f 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -15,7 +15,7 @@ open Declarations
 module Refset' : Set.S with type elt = global_reference
 module Refmap' : Map.S with type key = global_reference
 
-val safe_basename_of_global : global_reference -> identifier
+val safe_basename_of_global : global_reference -> Id.t
 
 (*s Warning and Error messages. *)
 
@@ -30,7 +30,7 @@ val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
 val error_no_module_expr : module_path -> 'a
-val error_singleton_become_prop : identifier -> 'a
+val error_singleton_become_prop : Id.t -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
@@ -193,12 +193,12 @@ val extract_inductive :
   reference -> string -> string list -> string option -> unit
 
 
-type int_or_id = ArgInt of int | ArgId of identifier
+type int_or_id = ArgInt of int | ArgId of Id.t
 val extraction_implicit : reference -> int_or_id list -> unit
 
 (*s Table of blacklisted filenames *)
 
-val extraction_blacklist : identifier list -> unit
+val extraction_blacklist : Id.t list -> unit
 val reset_extraction_blacklist : unit -> unit
 val print_extraction_blacklist : unit -> Pp.std_ppcmds
 
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index d224f87df..093087511 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -116,7 +116,7 @@ type side = Hyp | Concl | Hint
 
 let no_atoms = (false,{positive=[];negative=[]})
 
-let dummy_id=VarRef (id_of_string "_") (* "_" cannot be parsed *)
+let dummy_id=VarRef (Id.of_string "_") (* "_" cannot be parsed *)
 
 let build_atoms gl metagen side cciterm =
   let trivial =ref false
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 753fdda72..48e60d798 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -25,7 +25,7 @@ let update_flags ()=
     red_flags:=
     Closure.RedFlags.red_add_transparent
       Closure.betaiotazeta
-      (Names.Idpred.full,Names.Cpred.complement !predref)
+      (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
   update_flags ();
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 414afad46..c7a582a0e 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -98,7 +98,7 @@ let rec collect_quantified seq=
 
 let dummy_constr=mkMeta (-1)
 
-let dummy_bvid=id_of_string "x"
+let dummy_bvid=Id.of_string "x"
 
 let mk_open_instance id gl m t=
   let env=pf_env gl in
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index 78a70ff51..bfebbaaf8 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -19,7 +19,7 @@ type 'a with_backtracking = tactic -> 'a
 
 val wrap : int -> bool -> seqtac
 
-val basename_of_global: global_reference -> identifier
+val basename_of_global: global_reference -> Id.t
 
 val clear_global: global_reference -> tactic
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 429a0a4a8..f8b1927a3 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -463,7 +463,7 @@ let mkAppL a =
 let rec fourier gl=
     Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
     let goal = strip_outer_cast (pf_concl gl) in
-    let fhyp=id_of_string "new_hyp_for_fourier" in
+    let fhyp=Id.of_string "new_hyp_for_fourier" in
     (* si le but est une inéquation, on introduit son contraire,
        et le but à prouver devient False *)
     try (let tac =
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c129306d2..ca73799c1 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -105,17 +105,17 @@ let make_refl_eq constructor type_of_t t  =
 
 type pte_info =
     {
-      proving_tac : (identifier list ->  Tacmach.tactic);
+      proving_tac : (Id.t list ->  Tacmach.tactic);
       is_valid : constr -> bool
     }
 
-type ptes_info = pte_info Idmap.t
+type ptes_info = pte_info Id.Map.t
 
 type 'a dynamic_info =
     {
       nb_rec_hyps : int;
-      rec_hyps : identifier list ;
-      eq_hyps : identifier list;
+      rec_hyps : Id.t list ;
+      eq_hyps : Id.t list;
       info : 'a
     }
 
@@ -361,7 +361,7 @@ let is_property (ptes_info:ptes_info) t_x full_type_of_hyp =
     if isVar pte && Array.for_all closed0 args
     then
       try
-	let info = Idmap.find (destVar pte) ptes_info in
+	let info = Id.Map.find (destVar pte) ptes_info in
 	info.is_valid full_type_of_hyp
       with Not_found -> false
     else false
@@ -406,7 +406,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
   do_rewrite eq_ids
 
 
-let rec_pte_id = id_of_string "Hrec"
+let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
   let coq_False = Coqlib.build_coq_False () in
   let coq_True = Coqlib.build_coq_True () in
@@ -430,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	if is_property ptes_infos t_x actual_real_type_of_hyp then
 	  begin
 	    let pte,pte_args =  (destApp t_x) in
-	    let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
+	    let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in
 	    let popped_t' = Termops.pop t' in
 	    let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
 	    let prove_new_type_of_hyp =
@@ -579,7 +579,7 @@ let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) =
       ]
       g
 
-let heq_id = id_of_string "Heq"
+let heq_id = Id.of_string "Heq"
 
 let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
   fun g ->
@@ -632,7 +632,7 @@ let my_orelse tac1 tac2 g =
 (*     observe (str "using snd tac since : " ++ Errors.print e); *)
     tac2 g
 
-let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
+let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
   let args = Array.of_list (List.map mkVar  args_id) in
   let instanciate_one_hyp hid =
     my_orelse
@@ -672,10 +672,10 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	tclMAP instanciate_one_hyp hyps;
 	(fun g ->
 	   let all_g_hyps_id =
-	     List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
+	     List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty
 	   in
 	   let remaining_hyps =
-	     List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
+	     List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps
 	   in
 	   do_prove remaining_hyps g
 	  )
@@ -885,7 +885,7 @@ let build_proof
 type static_fix_info =
     {
       idx : int;
-      name : identifier;
+      name : Id.t;
       types : types;
       offset : int;
       nb_realargs : int;
@@ -1042,7 +1042,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
       (fun na ->
 	 let new_id =
 	   match na with
-	       Name id -> fresh_id !avoid (string_of_id id)
+	       Name id -> fresh_id !avoid (Id.to_string id)
 	     | Anonymous -> fresh_id !avoid "H"
 	 in
 	 avoid := new_id :: !avoid;
@@ -1183,14 +1183,14 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		   in
 (* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
 (* 			      str " to " ++ Ppconstr.pr_id info.name); *)
-		   (Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info)
+		   (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info)
 		   )
 		0
-		(Idmap.empty,[])
+		(Id.Map.empty,[])
 		(List.rev princ_info.predicates)
 	    in
 	    pte_to_fix,List.rev rev_info
-	| _ -> Idmap.empty,[]
+	| _ -> Id.Map.empty,[]
     in
     let mk_fixes : tactic =
       let pre_info,infos = list_chop fun_num infos in
@@ -1224,7 +1224,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	let pte,pte_args = (decompose_app pte_app) in
 	try
 	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in
-	  let fix_info = Idmap.find  pte ptes_to_fix in
+	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
 	    [
@@ -1262,7 +1262,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		       build_proof
 			 interactive_proof
 			 (Array.to_list fnames)
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 		     in
 		     let prove_tac branches  =
 		       let dyn_infos =
@@ -1272,7 +1272,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			 }
 		       in
 		       observe_tac "cleaning" (clean_goal_with_heq
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 			 do_prove
 			 dyn_infos)
 		     in
@@ -1316,7 +1316,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		      build_proof
 			interactive_proof
 			(Array.to_list fnames)
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 		    in
 		    let prove_tac branches  =
 		      let dyn_infos =
@@ -1326,7 +1326,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			 }
 		      in
 		       clean_goal_with_heq
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 			 do_prove
 			 dyn_infos
 		    in
@@ -1413,7 +1413,7 @@ let rec rewrite_eqs_in_eqs eqs =
 	    (tclMAP
 	       (fun id gl ->
 		  observe_tac
-		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
+		    (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id))
 		    (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences
 			       true (* dep proofs also: *) true id (mkVar eq) false))
 		    gl
@@ -1427,7 +1427,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
     (tclTHENSEQ
        [
 	 backtrack_eqs_until_hrec hrec eqs;
-	 (* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *)
+	 (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
 	    (apply (mkVar hrec))
 	    [ tclTHENSEQ
@@ -1463,13 +1463,13 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 
 
 let is_valid_hypothesis predicates_name =
-  let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in
+  let predicates_name = List.fold_right Id.Set.add predicates_name Id.Set.empty in
   let is_pte typ =
     if isApp typ
     then
       let pte,_ = destApp typ in
       if isVar pte
-      then Idset.mem (destVar pte) predicates_name
+      then Id.Set.mem (destVar pte) predicates_name
       else false
     else false
   in
@@ -1491,7 +1491,7 @@ let prove_principle_for_gen
     fun na ->
       let new_id =
 	  match na with
-	    | Name id -> fresh_id !avoid (string_of_id id)
+	    | Name id -> fresh_id !avoid (Id.to_string id)
 	    | Anonymous -> fresh_id !avoid "H"
       in
       avoid := new_id :: !avoid;
@@ -1534,9 +1534,9 @@ let prove_principle_for_gen
   let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
-  let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in
+  let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
   let acc_rec_arg_id =
-    Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id)))))
+    Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
     tclTHEN (h_generalize (List.map mkVar l)) (clear l)
@@ -1580,7 +1580,7 @@ let prove_principle_for_gen
     let hyps = pf_ids_of_hyps gls in
       let hid =
 	next_ident_away_in_goal
-	  (id_of_string "prov")
+	  (Id.of_string "prov")
 	  hyps
       in
       tclTHENSEQ
@@ -1669,14 +1669,14 @@ let prove_principle_for_gen
 	     is_valid = is_valid_hypothesis predicates_names
 	   }
 	 in
-	 let ptes_info : pte_info Idmap.t =
+	 let ptes_info : pte_info Id.Map.t =
 	   List.fold_left
 	     (fun map pte_id ->
-		Idmap.add pte_id
+		Id.Map.add pte_id
 		  pte_info
 		  map
 	     )
-	     Idmap.empty
+	     Id.Map.empty
 	     predicates_names
 	 in
 	 let make_proof rec_hyps =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 533fbfaaa..1d30ce9a6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -41,7 +41,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env = Global.env () in
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:identifier list) (predicates:rel_context)  : rel_context =
+  let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context)  : rel_context =
     match predicates with
     | [] -> []
     |(Name x,v,t)::predicates ->
@@ -83,10 +83,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
   let is_pte =
-    let set = List.fold_right Idset.add ptes_vars Idset.empty in
+    let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
     fun t ->
       match kind_of_term t with
-	| Var id -> Idset.mem id set
+	| Var id -> Id.Set.mem id set
 	| _ -> false
   in
   let pre_princ =
@@ -114,7 +114,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       | Construct((_,num),_) -> num
       | _ -> assert false
   in
-  let dummy_var = mkVar (id_of_string "________") in
+  let dummy_var = mkVar (Id.of_string "________") in
   let mk_replacement c i args =
     let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in
 (*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
@@ -284,7 +284,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
      observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
   let new_princ_name =
-    next_ident_away_in_goal (id_of_string "___________princ_________") []
+    next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
   begin
     Lemmas.start_proof
@@ -366,7 +366,7 @@ let generate_functional_principle
       begin
 	try
 	  let id = Pfedit.get_current_proof_name () in
-	  let s = string_of_id id in
+	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
 	  then if String.sub s 0 n = "___________princ_________"
@@ -519,7 +519,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
       begin
 	try
 	  let id = Pfedit.get_current_proof_name () in
-	  let s = string_of_id id in
+	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
 	  then if String.sub s 0 n = "___________princ_________"
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 00d130d28..a16b834f8 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -10,7 +10,7 @@ val generate_functional_principle :
   (* *)
   sorts array option ->
   (* Name of the new principle *)
-  (identifier) option ->
+  (Id.t) option ->
   (* the compute functions to use   *)
   constant array ->
   (* We prove the nth- principle *)
@@ -29,6 +29,6 @@ exception No_graph_found
 
 val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list
 
-val build_scheme : (identifier*Libnames.reference*glob_sort) list ->  unit
-val build_case_scheme : (identifier*Libnames.reference*glob_sort)  ->  unit
+val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
+val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2fdf62d26..ef2276134 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -368,7 +368,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list =
     an occurence of function [id] in the conclusion of goal [g]. If
     [id]=[None] then calls to any function are selected. In any case
     [heuristic] is used to select the most pertinent occurrence. *)
-let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list)
+let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
     (nexttac:Proof_type.tactic) g =
   let test = match oid with
     | Some id ->
@@ -468,10 +468,10 @@ VERNAC COMMAND EXTEND MergeFunind
        let ar2 = List.length (fst (decompose_prod f2type)) in
        let _ =
 	 if ar1 <> List.length cl1 then
-	   Errors.error ("not the right number of arguments for " ^ string_of_id id1) in
+	   Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in
        let _ =
 	 if ar2 <> List.length cl2 then
-	   Errors.error ("not the right number of arguments for " ^ string_of_id id2) in
+	   Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in
        Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
      ]
 END
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 593e274fb..cf7d8e8fe 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -57,7 +57,7 @@ type 'a build_entry_pre_return =
 type 'a build_entry_return =
     {
       result : 'a build_entry_pre_return list;
-      to_avoid : identifier list
+      to_avoid : Id.t list
     }
 
 (*
@@ -114,9 +114,9 @@ let ids_of_binder =  function
 let rec change_vars_in_binder mapping = function
     [] -> []
   | (bt,t)::l ->
-      let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in
+      let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
       (bt,change_vars mapping t)::
-	(if idmap_is_empty new_mapping
+	(if Id.Map.is_empty new_mapping
 	 then l
 	 else change_vars_in_binder new_mapping l
 	)
@@ -138,23 +138,23 @@ let apply_args ctxt body args =
   let need_convert avoid  bt =
     List.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
+  let next_name_away (na:name) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
     match na with
        | Name id when List.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
-	   Name new_id,Idmap.add id new_id mapping,new_id::avoid
+	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
        | _ -> na,mapping,avoid
   in
-  let next_bt_away bt (avoid:identifier list) =
+  let next_bt_away bt (avoid:Id.t list) =
     match bt with
       | LetIn na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  LetIn new_na,mapping,new_avoid
       | Prod na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  Prod new_na,mapping,new_avoid
       | Lambda na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  Lambda new_na,mapping,new_avoid
   in
   let rec do_apply avoid ctxt body args =
@@ -173,7 +173,7 @@ let apply_args ctxt body args =
 	      let new_avoid =  id::avoid in
 	      let new_id = Namegen.next_ident_away id new_avoid in
 	      let new_avoid' = new_id :: new_avoid in
-	      let mapping = Idmap.add id new_id Idmap.empty in
+	      let mapping = Id.Map.add id new_id Id.Map.empty in
 	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
 	      let new_body = change_vars mapping body in
 	      new_avoid',new_ctxt',new_body,new_id
@@ -477,7 +477,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			      GApp(Loc.ghost,t,l)
 		in
 		build_entry_lc env funnames avoid (aux f args)
-	    | GVar(_,id) when Idset.mem id funnames ->
+	    | GVar(_,id) when Id.Set.mem id funnames ->
 		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
 		   then we create a fresh variable [res],
 		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
@@ -725,7 +725,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	   (will be used in the following recursive calls)
 	*)
 	let new_env = List.fold_right2 add_pat_variables patl types env in
-	let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list =
+	let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
 	  List.map2
 	    (fun pat typ ->
 	       fun avoid pat'_as_term ->
@@ -787,7 +787,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
 		   (fun id  acc ->
-		      if Idset.mem id this_pat_ids
+		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
 		      let raw_typ_of_id =
@@ -835,7 +835,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 
 let is_res id =
   try
-    String.sub (string_of_id id) 0 4 = "_res"
+    String.sub (Id.to_string id) 0 4 = "_res"
   with Invalid_argument _ -> false
 
 
@@ -901,7 +901,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    (depth + 1) b
 			in
 			mkGProd(n,new_t,new_b),
-			Idset.filter not_free_in_t id_to_exclude
+			Id.Set.filter not_free_in_t id_to_exclude
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
@@ -1019,7 +1019,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
 		     if keep_eq then
 		     mkGProd(n,t,new_b),id_to_exclude
-		     else new_b, Idset.add id id_to_exclude
+		     else new_b, Id.Set.add id id_to_exclude
 		  *)
 	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
 		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
@@ -1051,10 +1051,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (depth + 1) b
 		in
 		match n with
-		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Idset.remove id
-			(Idset.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Id.Set.remove id
+			(Id.Set.filter not_free_in_t id_to_exclude)
+		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
@@ -1067,10 +1067,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (depth + 1) b
 		in
 		match n with
-		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Idset.remove id
-			(Idset.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Id.Set.remove id
+			(Id.Set.filter not_free_in_t id_to_exclude)
+		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLambda(_,n,k,t,b) ->
 	begin
@@ -1087,11 +1087,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (args@[mkGVar id])new_crossed_types
 		    (depth + 1 ) b
 		in
-		if Idset.mem id id_to_exclude && depth >= nb_args
+		if Id.Set.mem id id_to_exclude && depth >= nb_args
 		then
-		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
-		  GProd(Loc.ghost,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly "Should not have an anonymous function here"
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
@@ -1108,10 +1108,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (t::crossed_types)
 	      (depth + 1 ) b in
 	  match n with
-	    | Name id when Idset.mem id id_to_exclude && depth >= nb_args  ->
-		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
+		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 	    | _ -> GLetIn(Loc.ghost,n,t,new_b),
-		Idset.filter not_free_in_t id_to_exclude
+		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(_,nal,(na,rto),t,b) ->
 	assert (rto=None);
@@ -1133,15 +1133,15 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      (depth + 1) b
 	  in
 (* 	  match n with  *)
-(* 	    | Name id when Idset.mem id id_to_exclude ->  *)
-(* 		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
+(* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
+(* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
 	  GLetTuple(Loc.ghost,nal,(na,None),t,new_b),
-		Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
+		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
 	end
 
-    | _ -> mkGApp(mkGVar  relname,args@[rt]),Idset.empty
+    | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
 
 (* debuging wrapper *)
@@ -1164,7 +1164,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 *)
 let rec compute_cst_params relnames params = function
   | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
-  | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames ->
+  | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames ->
       compute_cst_params_from_app [] (params,rtl)
   | GApp(_,f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
@@ -1182,7 +1182,7 @@ and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
     | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl'
-	when id_ord id id' == 0 && not is_defined ->
+	when Id.compare id id' == 0 && not is_defined ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
@@ -1233,7 +1233,7 @@ let do_build_inductive
     (rtl:glob_constr list) =
   let _time1 = System.get_time () in
 (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
-  let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
+  let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
   let funnames = Array.of_list funnames in
   let funsargs = Array.of_list funsargs in
   let returned_types = Array.of_list returned_types in
@@ -1244,7 +1244,7 @@ let do_build_inductive
     Ensures by: obvious
     i*)
   let relnames = Array.map mk_rel_id funnames in
-  let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in
+  let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
   (* Construction of the pseudo constructors *)
   let env =
     Array.fold_right
@@ -1264,12 +1264,12 @@ let do_build_inductive
 	(fun (n,t,is_defined) acc ->
 	   if is_defined
 	   then
-	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t,
+	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
 			      acc)
 	   else
 	     Constrexpr.CProdN
 	       (Loc.ghost,
-		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
 		acc
 	       )
 	)
@@ -1307,9 +1307,9 @@ let do_build_inductive
     (*i The next call to mk_rel_id is valid since we are constructing the graph
       Ensures by: obvious
       i*)
-    id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
+    Id.of_string ((Id.to_string (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
   in
-  let rel_constructors i rt : (identifier*glob_constr) list =
+  let rel_constructors i rt : (Id.t*glob_constr) list =
     next_constructor_id := (-1);
     List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
   in
@@ -1330,12 +1330,12 @@ let do_build_inductive
       (fun (n,t,is_defined) acc ->
 	 if is_defined
 	 then
-	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t,
+	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
 			    acc)
 	 else
 	   Constrexpr.CProdN
 	   (Loc.ghost,
-	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
 	    acc
 	   )
       )
@@ -1352,10 +1352,10 @@ let do_build_inductive
       (fun (n,t,is_defined) ->
 	 if is_defined
 	 then
-	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Idset.empty t)
+	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t)
 	 else
 	 Constrexpr.LocalRawAssum
-	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
+	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
   in
@@ -1365,7 +1365,7 @@ let do_build_inductive
 	 false,((Loc.ghost,id),
 		Flags.with_option
 		  Flags.raw_print
-		  (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t)
+		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t)
 	       )
       ))
       (rel_constructors)
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index b8e7b3ab4..87fcb1022 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -8,7 +8,7 @@
 *)
 
 val build_inductive :
-  Names.identifier list -> (* The list of function name *)
+  Names.Id.t list -> (* The list of function name *)
   (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index f678b898b..7785cbe59 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -6,9 +6,6 @@ open Names
 open Decl_kinds
 open Misctypes
 
-(* Ocaml 3.06 Map.S does not handle is_empty *)
-let idmap_is_empty m = m = Idmap.empty
-
 (*
    Some basic functions to rebuild glob_constr
    In each of them the location is Loc.ghost
@@ -119,7 +116,7 @@ let rec glob_make_or_list = function
 let remove_name_from_mapping mapping na =
   match na with
     | Anonymous -> mapping
-    | Name id -> Idmap.remove id mapping
+    | Name id -> Id.Map.remove id mapping
 
 let change_vars =
   let rec change_vars mapping rt =
@@ -128,7 +125,7 @@ let change_vars =
       | GVar(loc,id) ->
 	  let new_id =
 	    try
-	      Idmap.find id mapping
+	      Id.Map.find id mapping
 	    with Not_found -> id
 	  in
 	  GVar(loc,new_id)
@@ -187,8 +184,8 @@ let change_vars =
 	  GCast(loc,change_vars mapping b,
 		Miscops.map_cast_type (change_vars mapping) c)
   and change_vars_br mapping ((loc,idl,patl,res) as br) =
-    let new_mapping = List.fold_right Idmap.remove idl mapping in
-    if idmap_is_empty new_mapping
+    let new_mapping = List.fold_right Id.Map.remove idl mapping in
+    if Id.Map.is_empty new_mapping
     then br
     else (loc,idl,patl,change_vars new_mapping res)
   in
@@ -200,27 +197,27 @@ let rec alpha_pat excluded pat =
   match pat with
     | PatVar(loc,Anonymous) ->
 	let new_id = Indfun_common.fresh_id excluded "_x" in
-	PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty
+	PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty
     | PatVar(loc,Name id) ->
 	if List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
 	  PatVar(loc,Name new_id),(new_id::excluded),
-	(Idmap.add id new_id Idmap.empty)
-	else pat,excluded,Idmap.empty
+	(Id.Map.add id new_id Id.Map.empty)
+	else pat,excluded,Id.Map.empty
     | PatCstr(loc,constr,patl,na) ->
 	let new_na,new_excluded,map =
 	  match na with
 	    | Name id when List.mem id excluded ->
 		let new_id = Namegen.next_ident_away id excluded in
-		Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
-	    | _ -> na,excluded,Idmap.empty
+		Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
+	    | _ -> na,excluded,Id.Map.empty
 	in
 	let new_patl,new_excluded,new_map =
 	  List.fold_left
 	    (fun (patl,excluded,map) pat ->
 	       let new_pat,new_excluded,new_map = alpha_pat excluded pat in
-	       (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map)
+	       (new_pat::patl,new_excluded,Id.Map.fold Id.Map.add new_map map)
 	    )
 	    ([],new_excluded,map)
 	    patl
@@ -232,9 +229,9 @@ let alpha_patl excluded patl  =
     List.fold_left
       (fun (patl,excluded,map) pat ->
 	 let new_pat,new_excluded,new_map = alpha_pat excluded pat in
-	 new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map)
+	 new_pat::patl,new_excluded,(Id.Map.fold Id.Map.add new_map map)
       )
-      ([],excluded,Idmap.empty)
+      ([],excluded,Id.Map.empty)
       patl
   in
   (List.rev patl,new_excluded,map)
@@ -266,7 +263,7 @@ let rec alpha_rt excluded rt =
     match rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt
       | GLambda(loc,Anonymous,k,t,b) ->
-	  let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in
+	  let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
 	  let new_excluded = new_id :: excluded in
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
@@ -285,7 +282,7 @@ let rec alpha_rt excluded rt =
 	  if new_id = id
 	  then t,b
 	  else
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
 	    (t,replace b)
 	in
 	let new_excluded = new_id::excluded in
@@ -299,7 +296,7 @@ let rec alpha_rt excluded rt =
 	  if new_id = id
 	  then t,b
 	  else
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
 	    (t,replace b)
 	in
 	let new_t = alpha_rt new_excluded t in
@@ -311,7 +308,7 @@ let rec alpha_rt excluded rt =
 	  if new_id = id
 	  then t,b
 	  else
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
 	    (t,replace b)
 	in
 	let new_excluded = new_id::excluded in
@@ -332,14 +329,14 @@ let rec alpha_rt excluded rt =
 		     then
 		       na::nal,id::excluded,mapping
 		     else
-		       (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping)
+		       (Name new_id)::nal,id::excluded,(Id.Map.add id new_id mapping)
 	    )
-	    ([],excluded,Idmap.empty)
+	    ([],excluded,Id.Map.empty)
 	    nal
 	in
 	let new_nal = List.rev rev_new_nal in
 	let new_rto,new_t,new_b =
-	  if idmap_is_empty mapping
+	  if Id.Map.is_empty mapping
 	  then rto,t,b
 	  else let replace = change_vars mapping in
 	  (Option.map replace rto, t,replace b)
@@ -387,14 +384,14 @@ and alpha_br excluded (loc,ids,patl,res) =
 let is_free_in id =
   let rec is_free_in = function
     | GRef _ ->  false
-    | GVar(_,id') -> id_ord id' id == 0
+    | GVar(_,id') -> Id.compare id' id == 0
     | GEvar _ -> false
     | GPatVar _ -> false
     | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
     | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) ->
 	let check_in_b =
 	  match n with
-	    | Name id' -> id_ord id' id <> 0
+	    | Name id' -> Id.compare id' id <> 0
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
@@ -451,7 +448,7 @@ let replace_var_by_term x_id term =
   let rec replace_var_by_pattern rt =
     match rt with
       | GRef _ -> rt
-      | GVar(_,id) when id_ord id x_id == 0 -> term
+      | GVar(_,id) when Id.compare id x_id == 0 -> term
       | GVar _ -> rt
       | GEvar _ -> rt
       | GPatVar _ -> rt
@@ -460,7 +457,7 @@ let replace_var_by_term x_id term =
 	       replace_var_by_pattern rt',
 	       List.map replace_var_by_pattern rtl
 	      )
-      | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | GLambda(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt
       | GLambda(loc,name,k,t,b) ->
 	  GLambda(loc,
 		  name,
@@ -468,7 +465,7 @@ let replace_var_by_term x_id term =
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | GProd(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt
       | GProd(loc,name,k,t,b) ->
 	  GProd(loc,
 		  name,
@@ -476,7 +473,7 @@ let replace_var_by_term x_id term =
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+      | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt
       | GLetIn(loc,name,def,b) ->
 	  GLetIn(loc,
 		 name,
@@ -512,7 +509,7 @@ let replace_var_by_term x_id term =
 	  GCast(loc,replace_var_by_pattern b,
 		Miscops.map_cast_type replace_var_by_pattern c)
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
-    if List.exists (fun id -> id_ord id x_id == 0) idl
+    if List.exists (fun id -> Id.compare id x_id == 0) idl
     then br
     else (loc,idl,patl,replace_var_by_pattern res)
   in
@@ -573,13 +570,13 @@ let eq_cases_pattern pat1 pat2 =
 let ids_of_pat =
   let rec ids_of_pat ids = function
     | PatVar(_,Anonymous) -> ids
-    | PatVar(_,Name id) -> Idset.add id ids
+    | PatVar(_,Name id) -> Id.Set.add id ids
     | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl
   in
-  ids_of_pat Idset.empty
+  ids_of_pat Id.Set.empty
 
 let id_of_name = function
-  | Names.Anonymous -> id_of_string "x"
+  | Names.Anonymous -> Id.of_string "x"
   | Names.Name x -> x
 
 (* TODO: finish Rec caes *)
@@ -604,7 +601,7 @@ let ids_of_glob_constr c =
       | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
   in
   (* build the set *)
-  List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c)
+  List.fold_left (fun acc x -> Id.Set.add x acc) Id.Set.empty (ids_of_glob_constr [] c)
 
 
 
@@ -678,7 +675,7 @@ let expand_as =
     match pat with
       | PatVar _ -> map
       | PatCstr(_,_,patl,Name id) ->
-	  Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl)
+	  Id.Map.add id (pattern_to_term pat) (List.fold_left add_as map patl)
       | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map rt =
@@ -687,7 +684,7 @@ let expand_as =
       | GVar(_,id) ->
 	  begin
 	    try
-	      Idmap.find id map
+	      Id.Map.find id map
 	    with Not_found -> rt
 	  end
       | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args)
@@ -710,4 +707,4 @@ let expand_as =
   and expand_as_br map (loc,idl,cpl,rt) =
     (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
   in
-  expand_as Idmap.empty
+  expand_as Id.Map.empty
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 9cf83df15..55d793e03 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,12 +1,8 @@
 open Glob_term
 open Misctypes
 
-(* Ocaml 3.06 Map.S does not handle is_empty *)
-val idmap_is_empty : 'a Names.Idmap.t -> bool
-
-
 (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
-val get_pattern_id : cases_pattern -> Names.identifier list
+val get_pattern_id : cases_pattern -> Names.Id.t list
 
 (* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
    [pat] must not contain occurences of anonymous pattern
@@ -18,7 +14,7 @@ val pattern_to_term : cases_pattern -> glob_constr
    In each of them the location is Util.Loc.ghost
 *)
 val mkGRef : Globnames.global_reference -> glob_constr
-val mkGVar : Names.identifier -> glob_constr
+val mkGVar : Names.Id.t -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
 val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr
 val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr
@@ -61,7 +57,7 @@ val  glob_make_or_list : glob_constr list -> glob_constr
 
 
 (* Replace the var mapped in the glob_constr/context *)
-val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr
+val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr
 
 
 
@@ -73,27 +69,27 @@ val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr
    [avoid] with the variables appearing in the result.
 *)
   val alpha_pat :
-    Names.Idmap.key list ->
+    Names.Id.Map.key list ->
     Glob_term.cases_pattern ->
-    Glob_term.cases_pattern * Names.Idmap.key list *
-      Names.identifier Names.Idmap.t
+    Glob_term.cases_pattern * Names.Id.Map.key list *
+      Names.Id.t Names.Id.Map.t
 
 (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
    conventions and  does not share bound variables with avoid
 *)
-val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
+val alpha_rt : Names.Id.t list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
-val alpha_br : Names.identifier list ->
-    Loc.t * Names.identifier list * Glob_term.cases_pattern list *
+val alpha_br : Names.Id.t list ->
+    Loc.t * Names.Id.t list * Glob_term.cases_pattern list *
     Glob_term.glob_constr ->
-    Loc.t * Names.identifier list * Glob_term.cases_pattern list *
+    Loc.t * Names.Id.t list * Glob_term.cases_pattern list *
     Glob_term.glob_constr
 
 
 (* Reduction function *)
 val replace_var_by_term  :
-  Names.identifier ->
+  Names.Id.t ->
   Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
 
 
@@ -101,7 +97,7 @@ val replace_var_by_term  :
 (*
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
-val is_free_in : Names.identifier -> glob_constr -> bool
+val is_free_in : Names.Id.t -> glob_constr -> bool
 
 
 val are_unifiable : cases_pattern -> cases_pattern -> bool
@@ -110,13 +106,13 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
 
 
 (*
-   ids_of_pat : cases_pattern -> Idset.t
+   ids_of_pat : cases_pattern -> Id.Set.t
    returns the set of variables appearing in a pattern
 *)
-val   ids_of_pat : cases_pattern -> Names.Idset.t
+val   ids_of_pat : cases_pattern -> Names.Id.Set.t
 
 (* TODO: finish this function (Fix not treated) *)
-val ids_of_glob_constr: glob_constr -> Names.Idset.t
+val ids_of_glob_constr: glob_constr -> Names.Id.Set.t
 
 (*
    removing let_in construction in a glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 22da1a966..f922b2f60 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -85,19 +85,19 @@ let functional_induction with_clean c princl pat =
     let princ_vars =
       List.fold_right
 	(fun a acc ->
-	  try Idset.add (destVar a) acc
+	  try Id.Set.add (destVar a) acc
 	  with _ -> acc
 	)
 	args
-	Idset.empty
+	Id.Set.empty
     in
-    let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in
-    let old_idl = Idset.diff old_idl princ_vars in
+    let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in
+    let old_idl = Id.Set.diff old_idl princ_vars in
     let subst_and_reduce g =
       if with_clean
       then
 	let idl =
-	  List.filter (fun id -> not (Idset.mem id old_idl))
+	  List.filter (fun id -> not (Id.Set.mem id old_idl))
 	    (Tacmach.pf_ids_of_hyps g)
 	in
 	let flag =
@@ -152,7 +152,7 @@ let build_newrecursive
         let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
-        (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls))
+        (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
@@ -185,8 +185,8 @@ let build_newrecursive l =
 
 (* Checks whether or not the mutual bloc is recursive *)
 let is_rec names =
-  let names = List.fold_right Idset.add names Idset.empty in
-  let check_id id names =  Idset.mem id names in
+  let names = List.fold_right Id.Set.add names Id.Set.empty in
+  let check_id id names =  Id.Set.mem id names in
   let rec lookup names = function
     | GVar(_,id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
@@ -195,11 +195,11 @@ let is_rec names =
     | GIf(_,b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
     | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b)  ->
-	lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
+	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
     | GLetTuple(_,nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
-	     (fun acc na -> Nameops.name_fold Idset.remove na acc)
+	     (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
 	     names
 	     nal
 	  )
@@ -209,7 +209,7 @@ let is_rec names =
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
   and lookup_br names (_,idl,_,rt) =
-    let new_names = List.fold_right Idset.remove idl names in
+    let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
   in
   lookup names
@@ -460,9 +460,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
     match wf_rel_expr_opt with 
       | None ->
 	  let ltof =
-	    let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in
+	    let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) in
 	    Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path
-			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
+			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
 	  in
 	  let fun_from_mes =
 	    let applied_mes =
@@ -475,8 +475,8 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	  wf_rel_from_mes,true
       | Some wf_rel_expr -> 
 	  let wf_rel_with_mes = 
-	    let a = Names.id_of_string "___a" in 
-	    let b = Names.id_of_string "___b" in 
+	    let a = Names.Id.of_string "___a" in 
+	    let b = Names.Id.of_string "___b" in 
 	    Constrexpr_ops.mkLambdaC(
 	      [Loc.ghost,Name a;Loc.ghost,Name b],
 	      Constrexpr.Default Explicit,
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index fb9116cc2..2d50adf00 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -4,7 +4,7 @@ open Libnames
 open Globnames
 open Refiner
 open Hiddentac 
-let mk_prefix pre id = id_of_string (pre^(string_of_id id))
+let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
 let mk_rel_id = mk_prefix "R_"
 let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
 let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
@@ -16,7 +16,7 @@ let msgnl m =
 let invalid_argument s = raise (Invalid_argument s)
 
 
-let fresh_id avoid s = Namegen.next_ident_away_in_goal (id_of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
@@ -116,7 +116,7 @@ let const_of_id id =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
   try Nametab.locate_constant princ_ref
-  with Not_found -> Errors.error ("cannot find "^ string_of_id id)
+  with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
@@ -133,8 +133,8 @@ let coq_constant s =
 
 let find_reference sl s =
     (Nametab.locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
+			   (List.map Id.of_string (List.rev sl)))
+	       (Id.of_string s)));;
 
 let eq = lazy(coq_constant "eq")
 let refl_equal = lazy(coq_constant "eq_refl")
@@ -510,8 +510,8 @@ let jmeq_refl () =
 let h_intros l =
   tclMAP h_intro l
 
-let h_id = id_of_string "h"
-let hrec_id = id_of_string "hrec"
+let h_id = Id.of_string "h"
+let hrec_id = Id.of_string "hrec"
 let well_founded = function () -> (coq_constant "well_founded")
 let acc_rel = function () -> (coq_constant "Acc")
 let acc_inv_id = function () -> (coq_constant "Acc_inv")
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 8f80c072c..7d0f5a00e 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -5,23 +5,23 @@ open Pp
    The mk_?_id function build different name w.r.t. a function
    Each of their use is justified in the code
 *)
-val mk_rel_id : identifier -> identifier
-val mk_correct_id : identifier -> identifier
-val mk_complete_id : identifier -> identifier
-val mk_equation_id : identifier -> identifier
+val mk_rel_id : Id.t -> Id.t
+val mk_correct_id : Id.t -> Id.t
+val mk_complete_id : Id.t -> Id.t
+val mk_equation_id : Id.t -> Id.t
 
 
 val msgnl : std_ppcmds -> unit
 
 val invalid_argument : string -> 'a
 
-val fresh_id : identifier list -> string -> identifier
-val fresh_name : identifier list -> string -> name
-val get_name : identifier list -> ?default:string -> name -> name
+val fresh_id : Id.t list -> string -> Id.t
+val fresh_name : Id.t list -> string -> name
+val get_name : Id.t list -> ?default:string -> name -> name
 
 val array_get_start : 'a array -> 'a array
 
-val id_of_name : name -> identifier
+val id_of_name : name -> Id.t
 
 val locate_ind : Libnames.reference -> inductive
 val locate_constant : Libnames.reference -> constant
@@ -44,7 +44,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
 val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
 val refl_equal : Term.constr Lazy.t
-val const_of_id: identifier -> constant
+val const_of_id: Id.t -> constant
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
@@ -54,14 +54,14 @@ val jmeq_refl : unit -> Term.constr
 
 val new_save_named : bool -> unit
 
-val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Tacexpr.declaration_hook -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
 *)
 val get_proof_clean : bool ->
-  Names.identifier *
+  Names.Id.t *
     (Entries.definition_entry * Decl_kinds.goal_kind *
       unit Tacexpr.declaration_hook)
 
@@ -113,9 +113,9 @@ exception ToShow of exn
 
 val is_strict_tcc : unit -> bool
 
-val h_intros: Names.identifier list -> Proof_type.tactic
-val h_id :  Names.identifier
-val hrec_id :  Names.identifier
+val h_intros: Names.Id.t list -> Proof_type.tactic
+val h_id :  Names.Id.t
+val hrec_id :  Names.Id.t
 val acc_inv_id :  Term.constr Util.delayed
 val ltof_ref : Globnames.global_reference Util.delayed
 val well_founded_ltof : Term.constr Util.delayed
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 517a1ce9c..4a466175f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -126,8 +126,8 @@ let generate_type g_to_f f graph i =
   (*i We need to name the vars [res] and [fv] i*)
   let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
   let named_ctxt = List.map_filter filter fun_ctxt in
-  let res_id = Namegen.next_ident_away_in_goal (id_of_string "_res") named_ctxt in
-  let fv_id = Namegen.next_ident_away_in_goal (id_of_string "fv") (res_id :: named_ctxt) in
+  let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
+  let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in
   (*i we can then type the argument to be applied to the function [f] i*)
   let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in
   (*i
@@ -242,13 +242,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* The number of args of the function is then easilly computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
-    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the funcitonnal principle is defined in the
        environement and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -258,7 +258,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	(fun (_,_,br_type) ->
 	   List.map
 	     (fun id -> Loc.ghost, IntroIdentifier id)
-	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
     in
@@ -276,16 +276,16 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_right
 	(fun (_,pat) acc ->
 	     match pat with
-	       | Genarg.IntroIdentifier id -> Idset.add id acc
+	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
 	| _ -> anomaly "Not an identifier"
 	)
 	(List.nth intro_pats (pred i))
-	Idset.empty
+	Id.Set.empty
       in
 	let pre_args g =
 	List.fold_right
 	  (fun (id,b,t) pre_args ->
-	    if Idset.mem id this_branche_ids
+	    if Id.Set.mem id this_branche_ids
 	    then
 	      match b with
 		| None -> id::pre_args
@@ -299,7 +299,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let pre_tac g =
 	List.fold_right
 	  (fun (id,b,t) pre_tac ->
-	     if Idset.mem id this_branche_ids
+	     if Id.Set.mem id this_branche_ids
 	     then
 	       match b with
 		 | None -> pre_tac
@@ -383,7 +383,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let app_constructor g = applist((mkConstruct(constructor)),constructor_args g) in
       (* an apply the tactic *)
       let res,hres =
-	match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with
+	match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
 	  | [res;hres] -> res,hres
 	  | _ -> assert false
       in
@@ -466,7 +466,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	  princ_type
 	  (h_exact f_principle));
 	observe_tac "intro args_names" (tclMAP h_intro args_names);
-	(* observe_tac "titi" (pose_proof (Name (id_of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
+	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
 	tclTHEN_i
 	  (observe_tac "functional_induction" (
@@ -506,13 +506,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* The number of args of the function is then easilly computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
-    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the funcitonnal principle is defined in the
        environement and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -522,7 +522,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	(fun (_,_,br_type) ->
 	   List.map
 	     (fun id -> Loc.ghost, Genarg.IntroIdentifier id)
-	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
     in
@@ -540,17 +540,17 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_right
 	  (fun (_,pat) acc ->
 	     match pat with
-	       | Genarg.IntroIdentifier id -> Idset.add id acc
+	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
 	       | _ -> anomaly "Not an identifier"
 	  )
 	  (List.nth intro_pats (pred i))
-	  Idset.empty
+	  Id.Set.empty
       in
       (* and get the real args of the branch by unfolding the defined constant *)
       let pre_args,pre_tac =
 	List.fold_right
 	  (fun (id,b,t) (pre_args,pre_tac) ->
-	     if Idset.mem id this_branche_ids
+	     if Id.Set.mem id this_branche_ids
 	     then
 	       match b with
 		 | None -> (id::pre_args,pre_tac)
@@ -624,7 +624,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let app_constructor = applist((mkConstruct(constructor)),constructor_args) in
       (* an apply the tactic *)
       let res,hres =
-	match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with
+	match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
 	  | [res;hres] -> res,hres
 	  | _ -> assert false
       in
@@ -735,7 +735,7 @@ and intros_with_rewrite_aux : tactic =
 		  | App(eq,args) when (eq_constr eq eq_ind)  ->
  		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
-			let id = pf_get_new_id (id_of_string "y") g  in
+			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g
 		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
@@ -753,7 +753,7 @@ and intros_with_rewrite_aux : tactic =
 		      ] g
 		      else if isVar args.(1)
 		      then
-			let id = pf_get_new_id (id_of_string "y") g  in
+			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ h_intro id;
 				     generalize_dependent_of (destVar args.(1)) id;
 				     tclTRY (Equality.rewriteLR (mkVar id));
@@ -762,7 +762,7 @@ and intros_with_rewrite_aux : tactic =
 			  g
 		      else if isVar args.(2) 
 		      then 
-			let id = pf_get_new_id (id_of_string "y") g  in
+			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ h_intro id;
 				     generalize_dependent_of (destVar args.(2)) id;
 				     tclTRY (Equality.rewriteRL (mkVar id));
@@ -771,7 +771,7 @@ and intros_with_rewrite_aux : tactic =
 			  g
 		      else
 			begin
-			  let id = pf_get_new_id (id_of_string "y") g  in
+			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
 			    h_intro id;
 			    tclTRY (Equality.rewriteLR (mkVar id));
@@ -797,7 +797,7 @@ and intros_with_rewrite_aux : tactic =
 			intros_with_rewrite
 		      ] g
 		  | _ ->
-		      let id = pf_get_new_id (id_of_string "y") g  in
+		      let id = pf_get_new_id (Id.of_string "y") g  in
 		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
 	      end
 	  | LetIn _ ->
@@ -904,11 +904,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
        and compute a fresh name for each of them
     *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
-    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* and fresh names for res H and the principle (cf bug bug #1174) *)
     let res,hres,graph_principle_id =
-      match generate_fresh_id (id_of_string "z") ids 3 with
+      match generate_fresh_id (Id.of_string "z") ids 3 with
 	| [res;hres;graph_principle_id] -> res,hres,graph_principle_id
 	| _ -> assert false
     in
@@ -920,7 +920,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(fun (_,_,br_type) ->
 	   List.map
 	     (fun id -> id)
-	     (generate_fresh_id (id_of_string "y") ids (nb_prod br_type))
+	     (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type))
 	)
 	branches
     in
@@ -1059,7 +1059,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove correctness ("^(string_of_id f_id)^")")
+	   (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
 	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
@@ -1110,7 +1110,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove completeness ("^(string_of_id f_id)^")")
+	   (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
 	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
@@ -1187,7 +1187,7 @@ let revert_graph kn post_tac hid g =
 
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
-    let old_ids = List.fold_right Idset.add  (pf_ids_of_hyps g) Idset.empty in
+    let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let type_of_h = pf_type_of g (mkVar hid) in
     match kind_of_term type_of_h with
       | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ())  ->
@@ -1206,7 +1206,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    h_intro hid;
 	    Inv.inv FullInversion None (NamedHyp hid);
 	    (fun g ->
-	       let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in
+	       let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
 	    );
 	  ] g
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 485b5b280..089493079 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -53,10 +53,10 @@ let understand = Pretyping.understand Evd.empty (Global.env())
 
 (** Operations on names and identifiers *)
 let id_of_name = function
-    Anonymous -> id_of_string "H"
+    Anonymous -> Id.of_string "H"
   | Name id   -> id;;
-let name_of_string str = Name (id_of_string str)
-let string_of_name nme = string_of_id (id_of_name nme)
+let name_of_string str = Name (Id.of_string str)
+let string_of_name nme = Id.to_string (id_of_name nme)
 
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
@@ -75,7 +75,7 @@ let ident_global_exist id =
 
 (** [next_ident_fresh id] returns a fresh identifier (ie not linked in
     global env) with base [id]. *)
-let next_ident_fresh (id:identifier) =
+let next_ident_fresh (id:Id.t) =
     let res = ref id in
     while ident_global_exist !res do res := Nameops.lift_subscript !res done;
     !res
@@ -129,7 +129,7 @@ let prNamedRLDecl s lc =
     prstr "\n";
   end
 
-let showind (id:identifier) =
+let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
   let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
@@ -247,7 +247,7 @@ type 'a merged_arg =
 
 type merge_infos =
     {
-      ident:identifier; (** new inductive name *)
+      ident:Id.t; (** new inductive name *)
       mib1: mutual_inductive_body;
       oib1: one_inductive_body;
       mib2: mutual_inductive_body;
@@ -350,8 +350,8 @@ let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list =
 
 (** {1 Utilities for merging} *)
 
-let ind1name = id_of_string "__ind1"
-let ind2name = id_of_string "__ind2"
+let ind1name = Id.of_string "__ind1"
+let ind2name = Id.of_string "__ind2"
 
 (** Performs verifications on two graphs before merging: they must not
     be co-inductive, and for the moment they must not be mutual
@@ -374,11 +374,11 @@ let build_raw_params prms_decl avoid =
   let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in
   let res,_ = glob_decompose_prod dummy_glob_constr in
   let comblist = List.combine prms_decl res in
-  comblist, res , (avoid @ (Idset.elements (ids_of_glob_constr dummy_glob_constr)))
+  comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr)))
 *)
 
 let ids_of_rawlist avoid rawl =
-    List.fold_left Idset.union avoid (List.map ids_of_glob_constr rawl)
+    List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl)
 
 
 
@@ -456,7 +456,7 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
       ([],[],[],[]) arity_ctxt in
 (*  let arity_ctxt2 =
     build_raw_params oib2.mind_arity_ctxt
-      (Idset.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
+      (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
   let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
   let _ = prstr "\n\n\n" in
   let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
@@ -564,7 +564,7 @@ let build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift =
   List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
 
 
-let find_app (nme:identifier) ltyp =
+let find_app (nme:Id.t) ltyp =
   try
     ignore
       (List.map
@@ -650,16 +650,16 @@ let rec merge_types shift accrec1
     linked args [allargs2] to target args of [allargs1] as specified
     in [shift]. [allargs1] and [allargs2] are in reverse order.  Also
     returns the list of unlinked vars of [allargs2]. *)
-let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
+let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array)
     (lnk:int merged_arg array) =
   Array.fold_left_i
     (fun i acc e ->
       if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *)
       else
         match e with
-          | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc
+          | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc
           | _ -> acc)
-    Idmap.empty lnk
+    Id.Map.empty lnk
 
 let build_link_map allargs1 allargs2 lnk =
   let allargs1 =
@@ -742,18 +742,18 @@ let fresh_cstror_suffix , cstror_suffix_init =
 (** [merge_constructor_id id1 id2 shift] returns the identifier of the
     new constructor from the id of the two merged constructor and
     the merging info. *)
-let merge_constructor_id id1 id2 shift:identifier =
-  let id = string_of_id shift.ident ^ "_" ^ fresh_cstror_suffix () in
-  next_ident_fresh (id_of_string id)
+let merge_constructor_id id1 id2 shift:Id.t =
+  let id = Id.to_string shift.ident ^ "_" ^ fresh_cstror_suffix () in
+  next_ident_fresh (Id.of_string id)
 
 
 
 (** [merge_constructors lnk shift avoid] merges the two list of
     constructor [(name*type)]. These are translated to glob_constr
     first, each of them having distinct var names. *)
-let merge_constructors (shift:merge_infos) (avoid:Idset.t)
-    (typcstr1:(identifier * glob_constr) list)
-    (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list =
+let merge_constructors (shift:merge_infos) (avoid:Id.Set.t)
+    (typcstr1:(Id.t * glob_constr) list)
+    (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list =
   List.flatten
     (List.map
         (fun (id1,rawtyp1) ->
@@ -775,14 +775,14 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
   let mkrawcor nme avoid typ =
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
-    Detyping.detype false (Idset.elements avoid) [] substindtyp in
+    Detyping.detype false (Id.Set.elements avoid) [] substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
-  let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in
+  let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in
   let lcstr2 =
     Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in
-  let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in
+  let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in
 
   let params1 =
     try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
@@ -806,11 +806,11 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
 let merge_mutual_inductive_body
     (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) =
   (* Mutual not treated, we take first ind body of each. *)
-  merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
+  merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
 
 
 let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *)
-  Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x
+  Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x
 
 let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
   let params = prms2 @ prms1 in
@@ -842,7 +842,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     [rawlist], named ident.
     FIXME: params et cstr_expr (arity) *)
 let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
-    (rawlist:(identifier * glob_constr) list) =
+    (rawlist:(Id.t * glob_constr) list) =
   let lident = Loc.ghost, shift.ident in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
@@ -875,7 +875,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
   let _ = prstr "\nrawlist : " in
   let _ =
-    List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in
+    List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string nm) tp;prstr "\n") rawlist in
   let _ = prstr "\nend rawlist\n" in
 (* FIX: retransformer en constr ici
    let shift_prm =
@@ -892,7 +892,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
 
 
 (* Find infos on identifier id. *)
-let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
+let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
   let kn_of_id x =
     let f_ref = Libnames.Ident (Loc.ghost,x) in
     locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
@@ -909,8 +909,8 @@ let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
 
     Warning: For the moment, repetitions of an id in [args1] or
     [args2] are not supported. *)
-let merge (id1:identifier) (id2:identifier) (args1:identifier array)
-    (args2:identifier array) id : unit =
+let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array)
+    (args2:Id.t array) id : unit =
   let finfo1 = find_Function_infos_safe id1 in
   let finfo2 = find_Function_infos_safe id2 in
   (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a2f16dc6d..28752fe4f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -51,11 +51,11 @@ let coq_base_constant s =
 
 let find_reference sl s =
     (locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
+			   (List.map Id.of_string (List.rev sl)))
+	       (Id.of_string s)));;
 
 
-let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
+let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
   fun f_id kind value ->
     let ce = {const_entry_body = value;
               const_entry_secctx = None;
@@ -73,7 +73,7 @@ let def_of_const t =
 	     | _ -> assert false)
        with _ ->
 	 anomaly ("Cannot find definition of constant "^
-		    (string_of_id (id_of_label (con_label sp))))
+		    (Id.to_string (id_of_label (con_label sp))))
       )
      |_ -> assert false
 
@@ -86,8 +86,8 @@ let type_of_const t =
 let constant sl s =
   constr_of_global
     (locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
+			   (List.map Id.of_string (List.rev sl)))
+	       (Id.of_string s)));;
 let const_of_ref = function
     ConstRef kn -> kn
   | _ -> anomaly "ConstRef expected"
@@ -120,15 +120,15 @@ let pf_get_new_ids idl g =
 let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
     (pf_type_of gls c)
-let h'_id = id_of_string "h'"
-let teq_id = id_of_string "teq"
-let ano_id = id_of_string "anonymous"
-let x_id = id_of_string "x"
-let k_id = id_of_string "k"
-let v_id = id_of_string "v"
-let def_id = id_of_string "def"
-let p_id = id_of_string "p"
-let rec_res_id = id_of_string "rec_res";;
+let h'_id = Id.of_string "h'"
+let teq_id = Id.of_string "teq"
+let ano_id = Id.of_string "anonymous"
+let x_id = Id.of_string "x"
+let k_id = Id.of_string "k"
+let v_id = Id.of_string "v"
+let def_id = Id.of_string "def"
+let p_id = Id.of_string "p"
+let rec_res_id = Id.of_string "rec_res";;
 let lt = function () -> (coq_base_constant "lt")
 let le = function () -> (coq_base_constant "le")
 let ex = function () -> (coq_base_constant "ex")
@@ -202,7 +202,7 @@ let (value_f:constr list -> global_reference -> constr) =
     let body = understand Evd.empty env glob_body in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -300,7 +300,7 @@ let check_not_nested forbidden e =
   let rec check_not_nested e =  
     match kind_of_term e with 
       | Rel _ -> ()
-      | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^string_of_id x)
+      | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^Id.to_string x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -324,21 +324,21 @@ let check_not_nested forbidden e =
 type 'a infos = 
     { nb_arg : int; (* function number of arguments *)
       concl_tac : tactic; (* final tactic to finish proofs *)
-      rec_arg_id : identifier; (*name of the declared recursive argument *)
+      rec_arg_id : Id.t; (*name of the declared recursive argument *)
       is_mes : bool; (* type of recursion *)
-      ih : identifier; (* induction hypothesis name *)
-      f_id : identifier;  (* function name *)
+      ih : Id.t; (* induction hypothesis name *)
+      f_id : Id.t;  (* function name *)
       f_constr : constr;  (* function term *)
       f_terminate : constr; (* termination proof term *)
       func : global_reference; (* functionnal reference *)
       info : 'a;
       is_main_branch : bool; (* on the main branch or on a matched expression *)
       is_final : bool; (* final first order term or not *)
-      values_and_bounds : (identifier*identifier) list; 
-      eqs : identifier list; 
-      forbidden_ids : identifier list;
+      values_and_bounds : (Id.t*Id.t) list; 
+      eqs : Id.t list; 
+      forbidden_ids : Id.t list;
       acc_inv : constr lazy_t;
-      acc_id : identifier;
+      acc_id : Id.t;
       args_assoc : ((constr list)*constr) list;
     }
 
@@ -651,7 +651,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   introduced back later; the result is the pair of the tactic and the
   list of hypotheses that have been generalized and cleared. *)
 let mkDestructEq :
-  identifier list -> constr -> goal sigma -> tactic * identifier list =
+  Id.t list -> constr -> goal sigma -> tactic * Id.t list =
   fun not_on_hyp expr g ->
   let hyps = pf_hyps g in
   let to_revert =
@@ -1031,10 +1031,10 @@ let termination_proof_header is_mes input_type ids args_id relation
       in
       let relation = substl pre_rec_args relation in
       let input_type = substl pre_rec_args input_type in
-      let wf_thm = next_ident_away_in_goal (id_of_string ("wf_R")) ids in
+      let wf_thm = next_ident_away_in_goal (Id.of_string ("wf_R")) ids in
       let wf_rec_arg =
 	next_ident_away_in_goal
-	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
+	  (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))
 	  (wf_thm::ids)
       in
       let hrec = next_ident_away_in_goal hrec_id
@@ -1206,8 +1206,8 @@ let build_and_l l =
 
 
 let is_rec_res id =
-  let rec_res_name = string_of_id rec_res_id   in
-  let id_name = string_of_id id in
+  let rec_res_name = Id.to_string rec_res_id   in
+  let id_name = Id.to_string id in
   try
     String.sub id_name 0 (String.length rec_res_name) = rec_res_name
   with _ -> false
@@ -1384,7 +1384,7 @@ let com_terminate
 
 
 let start_equation (f:global_reference) (term_f:global_reference)
-  (cont_tactic:identifier list -> tactic) g =
+  (cont_tactic:Id.t list -> tactic) g =
   let ids = pf_ids_of_hyps g in
   let terminate_constr = constr_of_global term_f in
   let nargs = nb_prod (type_of_const terminate_constr) in
@@ -1397,7 +1397,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
                              Array.of_list (List.map mkVar x))));
     observe_tac (str "prove_eq") (cont_tactic x)] g;;
 
-let (com_eqn : int -> identifier ->
+let (com_eqn : int -> Id.t ->
        global_reference -> global_reference -> global_reference
 	 -> constr -> unit) =
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
@@ -1430,12 +1430,12 @@ let (com_eqn : int -> identifier ->
 		eqs = [];
 		forbidden_ids = [];
 		acc_inv = lazy (assert false);
-		acc_id = id_of_string "____";
+		acc_id = Id.of_string "____";
 		args_assoc = [];
-		f_id = id_of_string "______";
-		rec_arg_id = id_of_string "______";
+		f_id = Id.of_string "______";
+		rec_arg_id = Id.of_string "______";
 		is_mes = false;
-		ih = id_of_string "______";
+		ih = Id.of_string "______";
 	       }
 	  )
        ); 
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 1117e2597..2ef685203 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -4,11 +4,11 @@
 val tclUSER_if_not_mes : 
   Proof_type.tactic ->
   bool -> 
-  Names.identifier list option -> 
+  Names.Id.t list option -> 
   Proof_type.tactic
 val recursive_definition :  
 bool ->
-           Names.identifier ->
+           Names.Id.t ->
            Constrintern.internalization_env ->
            Constrexpr.constr_expr ->
            Constrexpr.constr_expr ->
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index aab237a23..d2d6a7b63 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -66,7 +66,7 @@ type 'cst formula =
   | C of 'cst formula * 'cst formula
   | D of 'cst formula * 'cst formula
   | N of 'cst formula
-  | I of 'cst formula * Names.identifier option * 'cst formula
+  | I of 'cst formula * Names.Id.t option * 'cst formula
 
 (**
   * Formula pretty-printer.
@@ -83,7 +83,7 @@ let rec pp_formula o f =
     | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)"
 	pp_formula f1
 	  (match n with
-	    | Some id -> Names.string_of_id id
+	    | Some id -> Names.Id.to_string id
 	    | None -> "") pp_formula f2
     | N(f) -> Printf.fprintf o "N(%a)" pp_formula f
 
@@ -1158,7 +1158,7 @@ struct
     | (e::l) ->
        let (name,expr,typ) = e in
         xset (Term.mkNamedLetIn
-               (Names.id_of_string name)
+               (Names.Id.of_string name)
                expr typ acc) l in
     xset concl l
 
@@ -1185,7 +1185,7 @@ let same_proof sg cl1 cl2 =
 
 let tags_of_clause tgs wit clause =
  let rec xtags tgs = function
-  | Mc.PsatzIn n -> Names.Idset.union tgs
+  | Mc.PsatzIn n -> Names.Id.Set.union tgs
      (snd (List.nth clause (CoqToCaml.nat n) ))
   | Mc.PsatzMulC(e,w) -> xtags tgs w
   | Mc.PsatzMulE (w1,w2) | Mc.PsatzAdd(w1,w2) -> xtags (xtags tgs w1) w2
@@ -1194,7 +1194,7 @@ let tags_of_clause tgs wit clause =
 
 (*let tags_of_cnf wits cnf =
  List.fold_left2 (fun acc w cl -> tags_of_clause acc w cl)
-  Names.Idset.empty wits cnf *)
+  Names.Id.Set.empty wits cnf *)
 
 let find_witness prover polys1 = try_any prover polys1
 
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 9bfebe348..851516945 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -85,7 +85,7 @@ let generalize_time = timing "Generalize"
 
 let new_identifier =
   let cpt = ref 0 in
-  (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s)
+  (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; Id.of_string s)
 
 let new_identifier_state =
   let cpt = ref 0 in
@@ -93,7 +93,7 @@ let new_identifier_state =
 
 let new_identifier_var =
   let cpt = ref 0 in
-  (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s)
+  (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; Id.of_string s)
 
 let new_id =
   let cpt = ref 0 in fun () -> incr cpt; !cpt
@@ -109,7 +109,7 @@ let display_var i = Printf.sprintf "X%d" i
 let intern_id,unintern_id =
   let cpt = ref 0 in
   let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in
-  (fun (name : identifier) ->
+  (fun (name : Id.t) ->
      try Hashtbl.find table name with Not_found ->
        let idx = !cpt in
        Hashtbl.add table name idx;
@@ -136,13 +136,13 @@ let rev_assoc k =
   loop
 
 let tag_hypothesis,tag_of_hyp, hyp_of_tag =
-  let l = ref ([]:(identifier * int) list) in
+  let l = ref ([]:(Id.t * int) list) in
   (fun h id -> l := (h,id):: !l),
   (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"),
   (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis")
 
 let hide_constr,find_constr,clear_tables,dump_tables =
-  let l = ref ([]:(constr * (identifier * identifier * bool)) list) in
+  let l = ref ([]:(constr * (Id.t * Id.t * bool)) list) in
   (fun h id eg b -> l := (h,(id,eg,b)):: !l),
   (fun h -> try List.assoc_f eq_constr h !l with Not_found -> failwith "find_contr"),
   (fun () -> l := []),
@@ -329,7 +329,7 @@ let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge)
 let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt)
 let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ())))
 
-let mk_var v = mkVar (id_of_string v)
+let mk_var v = mkVar (Id.of_string v)
 let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
 let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
 let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
@@ -370,7 +370,7 @@ type omega_proposition =
   | Kn
 
 type result =
-  | Kvar of identifier
+  | Kvar of Id.t
   | Kapp of omega_constant * constr list
   | Kimp of constr * constr
   | Kufo
@@ -527,7 +527,7 @@ let occurence path (t : constr) =
 let abstract_path typ path t =
   let term_occur = ref (mkRel 0) in
   let abstract = context (fun i t -> term_occur:= t; mkRel i) path t in
-  mkLambda (Name (id_of_string "x"), typ, abstract), !term_occur
+  mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
 
 let focused_simpl path gl =
   let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
@@ -539,7 +539,7 @@ type oformula =
   | Oplus of oformula * oformula
   | Oinv of  oformula
   | Otimes of oformula * oformula
-  | Oatom of identifier
+  | Oatom of Id.t
   | Oz of bigint
   | Oufo of constr
 
@@ -551,7 +551,7 @@ let rec oprint = function
   | Otimes (t1,t2) ->
       print_string "("; oprint t1; print_string "*";
       oprint t2; print_string ")"
-  | Oatom s -> print_string (string_of_id s)
+  | Oatom s -> print_string (Id.to_string s)
   | Oz i -> print_string (string_of_bigint i)
   | Oufo f -> print_string "?"
 
@@ -597,10 +597,10 @@ let clever_rewrite_base_poly typ p result theorem gl =
   let t =
     applist
       (mkLambda
-	 (Name (id_of_string "P"),
+	 (Name (Id.of_string "P"),
 	  mkArrow typ mkProp,
           mkLambda
-	    (Name (id_of_string "H"),
+	    (Name (Id.of_string "H"),
 	     applist (mkRel 1,[result]),
 	     mkApp (Lazy.force coq_eq_ind_r,
 		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
@@ -1007,9 +1007,9 @@ let rec clear_zero p = function
   | t -> [],t
 
 let replay_history tactic_normalisation =
-  let aux  = id_of_string "auxiliary" in
-  let aux1 = id_of_string "auxiliary_1" in
-  let aux2 = id_of_string "auxiliary_2" in
+  let aux  = Id.of_string "auxiliary" in
+  let aux1 = Id.of_string "auxiliary_1" in
+  let aux2 = Id.of_string "auxiliary_2" in
   let izero = mk_integer zero in
   let rec loop t =
     match t with
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index ee341cbc2..d94a7136a 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -39,7 +39,7 @@ END
 
 TACTIC EXTEND omega'
 | [ "omega" "with" ne_ident_list(l) ] ->
-    [ omega_tactic (List.map Names.string_of_id l) ]
+    [ omega_tactic (List.map Names.Id.to_string l) ]
 | [ "omega" "with" "*" ] -> [ omega_tactic ["nat";"positive";"N";"Z"] ]
 END
 
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 61a464c1c..4238037e7 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -189,10 +189,10 @@ let decomp_term c = kind_of_term (strip_outer_cast c)
   type [typ] *)
 
 let coerce_meta_out id =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   int_of_string (String.sub s 1 (String.length s - 1))
 let coerce_meta_in n =
-  id_of_string ("M" ^ string_of_int n)
+  Id.of_string ("M" ^ string_of_int n)
 
 let compute_lhs typ i nargsi =
   match kind_of_term typ with
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 5b57a0d17..92135d497 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -22,10 +22,10 @@ let string_of_global r =
   let prefix = match Names.repr_dirpath dp with
     | [] -> ""
     | m::_ ->
-      let s = Names.string_of_id m in
+      let s = Names.Id.to_string m in
       if List.mem s meaningful_submodule then s^"." else ""
   in
-  prefix^(Names.string_of_id (Nametab.basename_of_global r))
+  prefix^(Names.Id.to_string (Nametab.basename_of_global r))
 
 let destructurate t =
   let c, args = Term.decompose_app t in
@@ -36,7 +36,7 @@ let destructurate t =
 	Kapp (string_of_global (Globnames.ConstructRef csp), args)
     | Term.Ind isp, args ->
 	Kapp (string_of_global (Globnames.IndRef isp), args)
-    | Term.Var id,[] -> Kvar(Names.string_of_id id)
+    | Term.Var id,[] -> Kvar(Names.Id.to_string id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
 	Errors.error "Omega: Not a quantifier-free goal"
@@ -296,13 +296,13 @@ let coq_Zneg = lazy (bin_constant "Zneg")
 let recognize t =
   let rec loop t =
     let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
+    match Names.Id.to_string f,l with
        "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t))
      | "xO",[t] -> Bigint.mult Bigint.two (loop t)
      | "xH",[] -> Bigint.one
      | _ -> failwith "not a number" in
   let f,l = dest_const_apply t in
-    match Names.string_of_id f,l with
+    match Names.Id.to_string f,l with
         "Zpos",[t] -> loop t
       | "Zneg",[t] -> Bigint.neg (loop t)
       | "Z0",[] -> Bigint.zero
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 5a843e2b7..a68196e8c 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -37,6 +37,6 @@ END
 
 TACTIC EXTEND romega'
 | [ "romega" "with" ne_ident_list(l) ] ->
-    [ romega_tactic (List.map Names.string_of_id l) ]
+    [ romega_tactic (List.map Names.Id.to_string l) ]
 | [ "romega" "with" "*" ] -> [ romega_tactic ["nat";"positive";"N";"Z"] ]
 END
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e573f2006..e3674fae0 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -40,7 +40,7 @@ type occ_path = occ_step list
 
 (* chemin identifiant une proposition sous forme du nom de l'hypothèse et
    d'une liste de pas à partir de la racine de l'hypothèse *)
-type occurence = {o_hyp : Names.identifier; o_path : occ_path}
+type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
 
 (* \subsection{refiable formulas} *)
 type oformula =
@@ -137,7 +137,7 @@ type context_content =
 
 (* \section{Specific utility functions to handle base types} *)
 (* Nom arbitraire de l'hypothèse codant la négation du but final *)
-let id_concl = Names.id_of_string "__goal__"
+let id_concl = Names.Id.of_string "__goal__"
 
 (* Initialisation de l'environnement de réification de la tactique *)
 let new_environment () = {
@@ -746,7 +746,7 @@ let reify_gl env gl =
       (i,t) :: lhyps ->
 	let t' = oproposition_of_constr env (false,[],i,[]) gl t in
 	if !debug then begin
-	  Printf.printf "  %s: " (Names.string_of_id i);
+	  Printf.printf "  %s: " (Names.Id.to_string i);
 	  pprint stdout t';
 	  Printf.printf "\n"
 	end;
@@ -840,7 +840,7 @@ let display_systems syst_list =
 	 (List.map (function O_left -> "L" | O_right -> "R" | O_mono -> "M")
 	    oformula_eq.e_origin.o_path));
     Printf.printf "\n  Origin: %s (negated : %s)\n\n"
-      (Names.string_of_id oformula_eq.e_origin.o_hyp)
+      (Names.Id.to_string oformula_eq.e_origin.o_hyp)
       (if oformula_eq.e_negated then "yes" else "no") in
 
   let display_system syst =
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index e5fb646a4..f7e6ec020 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -18,7 +18,7 @@ val make_hyps :
     atom_env ->
     Proof_type.goal Tacmach.sigma ->
     Term.types list ->
-    (Names.identifier * Term.types option * Term.types) list ->
-    (Names.identifier * Proof_search.form) list
+    (Names.Id.t * Term.types option * Term.types) list ->
+    (Names.Id.t * Proof_search.form) list
 
 val rtauto_tac : Proof_type.tactic
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 717b19e2c..17ea6f2bf 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -119,19 +119,19 @@ END;;*)
 
 (*
 let closed_term_ast l =
-  TacFun([Some(id_of_string"t")],
+  TacFun([Some(Id.of_string"t")],
   TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
-  [Genarg.in_gen Genarg.wit_constr (mkVar(id_of_string"t"));
+  [Genarg.in_gen Genarg.wit_constr (mkVar(Id.of_string"t"));
    Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l])))
 *)
 let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in
-  TacFun([Some(id_of_string"t")],
+  TacFun([Some(Id.of_string"t")],
   TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term",
-  [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,id_of_string"t"),None);
+  [Genarg.in_gen Genarg.globwit_constr (GVar(Loc.ghost,Id.of_string"t"),None);
    Genarg.in_gen (Genarg.wit_list1 Genarg.globwit_ref) l])))
 (*
-let _ = add_tacdef false ((Loc.ghost,id_of_string"ring_closed_term"
+let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
 *)
 
 (****************************************************************************)
@@ -143,7 +143,7 @@ let ic c =
 let ty c = Typing.type_of (Global.env()) Evd.empty c
 
 let decl_constant na c =
-  mkConst(declare_constant (id_of_string na) (DefinitionEntry
+  mkConst(declare_constant (Id.of_string na) (DefinitionEntry
     { const_entry_body = c;
       const_entry_secctx = None;
       const_entry_type = None;
@@ -156,17 +156,17 @@ let ltac_call tac (args:glob_tactic_arg list) =
 
 (* Calling a locally bound tactic *)
 let ltac_lcall tac args =
-  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, id_of_string tac),args))
+  TacArg(Loc.ghost,TacCall(Loc.ghost, ArgVar(Loc.ghost, Id.of_string tac),args))
 
 let ltac_letin (x, e1) e2 =
-  TacLetIn(false,[(Loc.ghost,id_of_string x),e1],e2)
+  TacLetIn(false,[(Loc.ghost,Id.of_string x),e1],e2)
 
 let ltac_apply (f:glob_tactic_expr) (args:glob_tactic_arg list) =
   Tacinterp.eval_tactic
     (ltac_letin ("F", Tacexp f) (ltac_lcall "F" args))
 
 let ltac_record flds =
-  TacFun([Some(id_of_string"proj")], ltac_lcall "proj" flds)
+  TacFun([Some(Id.of_string"proj")], ltac_lcall "proj" flds)
 
 
 let carg c = TacDynamic(Loc.ghost,Pretyping.constr_in c)
@@ -178,7 +178,7 @@ let dummy_goal env =
    Evd.sigma = sigma}
 
 let exec_tactic env n f args =
-  let lid = List.tabulate(fun i -> id_of_string("x"^string_of_int i)) n in
+  let lid = List.tabulate(fun i -> Id.of_string("x"^string_of_int i)) n in
   let res = ref [||] in
   let get_res ist =
     let l = List.map (fun id ->  List.assoc id ist.lfun) lid in
@@ -244,11 +244,11 @@ let my_constant c =
   lazy (Coqlib.gen_constant_in_modules "Ring" plugin_modules c)
 
 let new_ring_path =
-  make_dirpath (List.map id_of_string ["Ring_tac";plugin_dir;"Coq"])
+  make_dirpath (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
   lazy(make_kn (MPfile new_ring_path) (make_dirpath []) (mk_label s))
 let znew_ring_path =
-  make_dirpath (List.map id_of_string ["InitialRing";plugin_dir;"Coq"])
+  make_dirpath (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
   lazy(make_kn (MPfile znew_ring_path) (make_dirpath []) (mk_label s))
 
@@ -689,8 +689,8 @@ let add_theory name rth eqth morphth cst_tac (pre,post) power sign div =
   let lemma1 = constr_of params.(3) in
   let lemma2 = constr_of params.(4) in
 
-  let lemma1 = decl_constant (string_of_id name^"_ring_lemma1") lemma1 in
-  let lemma2 = decl_constant (string_of_id name^"_ring_lemma2") lemma2 in
+  let lemma1 = decl_constant (Id.to_string name^"_ring_lemma1") lemma1 in
+  let lemma2 = decl_constant (Id.to_string name^"_ring_lemma2") lemma2 in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -826,7 +826,7 @@ END
 (***********************************************************************)
 
 let new_field_path =
-  make_dirpath (List.map id_of_string ["Field_tac";plugin_dir;"Coq"])
+  make_dirpath (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
   lazy(make_kn (MPfile new_field_path) (make_dirpath []) (mk_label s))
@@ -1049,11 +1049,11 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign odi
     match inj with
       | Some thm -> mkApp(constr_of params.(8),[|thm|])
       | None -> constr_of params.(7) in
-  let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in
-  let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in
-  let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in
-  let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in
-  let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in
+  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1") lemma1 in
+  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2") lemma2 in
+  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3") lemma3 in
+  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4") lemma4 in
+  let cond_lemma = decl_constant (Id.to_string name^"_lemma5") cond_lemma in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 03fbc7e98..958fdc649 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -16,9 +16,9 @@ open Coqlib
 
 exception Non_closed_ascii
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_kn dir id = Globnames.encode_mind (make_dir dir) (id_of_string id)
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
+let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let ascii_module = ["Coq";"Strings";"Ascii"]
 
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 94d4e0713..f86b56bc7 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -14,8 +14,8 @@ open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
-let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id)
+let make_dir l = Names.make_dirpath (List.map Names.Id.of_string (List.rev l))
+let make_path dir id = Libnames.make_path (make_dir dir) (Names.Id.of_string id)
 
 let make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
 let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index a40c966fe..f7d0091f3 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -19,14 +19,14 @@ exception Non_closed_number
 open Glob_term
 open Bigint
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
 let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
-let make_path dir id = Libnames.make_path dir (id_of_string id)
+let make_path dir id = Libnames.make_path dir (Id.of_string id)
 
 let r_path = make_path rdefinitions "R"
 
 (* TODO: temporary hack *)
-let make_path dir id = Globnames.encode_con dir (id_of_string id)
+let make_path dir id = Globnames.encode_con dir (Id.of_string id)
 
 let r_kn = make_path rdefinitions "R"
 let glob_R = ConstRef r_kn
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 8e5a07e0d..9faa6edd1 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -23,15 +23,15 @@ open Glob_term
 
 let binnums = ["Coq";"Numbers";"BinNums"]
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
+let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
 let make_kn dir id = Globnames.encode_mind dir id
 
-let positive_kn = make_kn (make_dir binnums) (id_of_string "positive")
+let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
 let glob_positive = IndRef (positive_kn,0)
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
@@ -93,7 +93,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
 (* Parsing N via scopes                                               *)
 (**********************************************************************)
 
-let n_kn = make_kn (make_dir binnums) (id_of_string "N")
+let n_kn = make_kn (make_dir binnums) (Id.of_string "N")
 let glob_n = IndRef (n_kn,0)
 let path_of_N0 = ((n_kn,0),1)
 let path_of_Npos = ((n_kn,0),2)
@@ -144,7 +144,7 @@ let _ = Notation.declare_numeral_interpreter "N_scope"
 (**********************************************************************)
 
 let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (id_of_string "Z")
+let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
 let glob_z = IndRef (z_kn,0)
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml
index 653c2b7bd..3e2c8ade7 100644
--- a/plugins/xml/acic.ml
+++ b/plugins/xml/acic.ml
@@ -34,7 +34,7 @@ type 'constr context_entry =
                                (* is not present in the DTD, but is needed   *)
                                (* to use Coq functions during exportation.   *)
 
-type 'constr hypothesis = identifier * 'constr context_entry
+type 'constr hypothesis = Id.t * 'constr context_entry
 type context = constr hypothesis list
 
 type conjecture = existential_key * context * constr
@@ -57,13 +57,13 @@ type obj =
     inductiveType list *                           (* inductive types ,      *)
     params * int                                   (*  parameters,n ind. pars*)
 and inductiveType =
- identifier * bool * constr *                 (* typename, inductive, arity *)
+ Id.t * bool * constr *                 (* typename, inductive, arity *)
   constructor list                            (*  constructors              *)
 and constructor =
- identifier * constr                          (* id, type *)
+ Id.t * constr                          (* id, type *)
 
 type aconstr =
-  | ARel       of id * int * id * identifier
+  | ARel       of id * int * id * Id.t
   | AVar       of id * uri
   | AEvar      of id * existential_key * aconstr list
   | ASort      of id * sorts
@@ -79,9 +79,9 @@ type aconstr =
   | AFix       of id * int * ainductivefun list
   | ACoFix     of id * int * acoinductivefun list
 and ainductivefun =
- id * identifier * int * aconstr * aconstr
+ id * Id.t * int * aconstr * aconstr
 and acoinductivefun =
- id * identifier * aconstr * aconstr
+ id * Id.t * aconstr * aconstr
 and explicit_named_substitution = id option * (uri * aconstr) list
 
 type acontext = (id * aconstr hypothesis) list
@@ -102,7 +102,7 @@ type aobj =
     anninductiveType list *                        (* inductive types ,      *)
     params * int                                   (*  parameters,n ind. pars*)
 and anninductiveType =
- id * identifier * bool * aconstr *           (* typename, inductive, arity *)
+ id * Id.t * bool * aconstr *           (* typename, inductive, arity *)
   annconstructor list                         (*  constructors              *)
 and annconstructor =
- identifier * aconstr                         (* id, type *)
+ Id.t * aconstr                         (* id, type *)
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index c03b13b5a..34bb1d51f 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -37,7 +37,7 @@ let print_term ids_to_inner_sorts =
        A.ARel (id,n,idref,b) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_empty "REL"
-          ["value",(string_of_int n) ; "binder",(N.string_of_id b) ;
+          ["value",(string_of_int n) ; "binder",(N.Id.to_string b) ;
            "id",id ; "idref",idref; "sort",sort]
      | A.AVar (id,uri) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
@@ -71,7 +71,7 @@ let print_term ids_to_inner_sorts =
                   ("id",id)::("type",sort)::
                   match binder with
                      Names.Anonymous -> []
-                   | Names.Name b -> ["binder",Names.string_of_id b]
+                   | Names.Name b -> ["binder",Names.Id.to_string b]
                  in
                   [< X.xml_nempty "decl" attrs (aux s) ; i >]
               ) [< >] prods ;
@@ -96,7 +96,7 @@ let print_term ids_to_inner_sorts =
                   ("id",id)::("type",sort)::
                   match binder with
                      Names.Anonymous -> []
-                   | Names.Name b -> ["binder",Names.string_of_id b]
+                   | Names.Name b -> ["binder",Names.Id.to_string b]
                  in
                   [< X.xml_nempty "decl" attrs (aux s) ; i >]
               ) [< >] lambdas ;
@@ -115,7 +115,7 @@ let print_term ids_to_inner_sorts =
                   ("id",id)::("sort",sort)::
                   match binder with
                      Names.Anonymous -> assert false
-                   | Names.Name b -> ["binder",Names.string_of_id b]
+                   | Names.Name b -> ["binder",Names.Id.to_string b]
                  in
                   [< X.xml_nempty "def" attrs (aux s) ; i >]
               ) [< >] letins ;
@@ -161,7 +161,7 @@ let print_term ids_to_inner_sorts =
               (fun i (id,fi,ai,ti,bi) ->
                 [< i ;
                    X.xml_nempty "FixFunction"
-                    ["id",id ; "name", (Names.string_of_id fi) ;
+                    ["id",id ; "name", (Names.Id.to_string fi) ;
                      "recIndex", (string_of_int ai)]
                     [< X.xml_nempty "type" [] [< aux ti >] ;
                        X.xml_nempty "body" [] [< aux bi >]
@@ -177,7 +177,7 @@ let print_term ids_to_inner_sorts =
               (fun i (id,fi,ti,bi) ->
                 [< i ;
                    X.xml_nempty "CofixFunction"
-                    ["id",id ; "name", Names.string_of_id fi]
+                    ["id",id ; "name", Names.Id.to_string fi]
                     [< X.xml_nempty "type" [] [< aux ti >] ;
                        X.xml_nempty "body" [] [< aux bi >]
                     >]
@@ -229,11 +229,11 @@ let print_object uri ids_to_inner_sorts =
                           [< (match t with
                                 n,A.Decl t ->
                                  X.xml_nempty "Decl"
-                                  ["id",hid;"name",Names.string_of_id n]
+                                  ["id",hid;"name",Names.Id.to_string n]
                                   (print_term ids_to_inner_sorts t)
                               | n,A.Def (t,_) ->
                                  X.xml_nempty "Def"
-                                  ["id",hid;"name",Names.string_of_id n]
+                                  ["id",hid;"name",Names.Id.to_string n]
                                   (print_term ids_to_inner_sorts t)
                              ) ;
                              i
@@ -315,7 +315,7 @@ let print_object uri ids_to_inner_sorts =
                   (fun i (id,typename,finite,arity,cons) ->
                     [< i ;
                        X.xml_nempty "InductiveType"
-                        ["id",id ; "name",Names.string_of_id typename ;
+                        ["id",id ; "name",Names.Id.to_string typename ;
                          "inductive",(string_of_bool finite)
                         ]
                         [< X.xml_nempty "arity" []
@@ -324,7 +324,7 @@ let print_object uri ids_to_inner_sorts =
                             (fun i (name,lc) ->
                               [< i ;
                                  X.xml_nempty "Constructor"
-                                  ["name",Names.string_of_id name]
+                                  ["name",Names.Id.to_string name]
                                   (print_term ids_to_inner_sorts lc)
                               >]) [<>] cons
                            )
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 62f7cc7cf..d817396f1 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -62,7 +62,7 @@ let get_uri_of_var v pvars =
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
        let dirpath = N.make_dirpath modules in
-        if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then
+        if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then
          modules
         else
          search_in_open_sections tl
@@ -75,7 +75,7 @@ let get_uri_of_var v pvars =
    in
     "cic:" ^
      List.fold_left
-      (fun i x -> "/" ^ N.string_of_id x ^ i) "" path
+      (fun i x -> "/" ^ N.Id.to_string x ^ i) "" path
 ;;
 
 type tag =
@@ -120,8 +120,8 @@ let subtract l1 l2 =
 let token_list_of_path dir id tag =
  let module N = Names in
   let token_list_of_dirpath dirpath =
-   List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
-  token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]
+   List.rev_map N.Id.to_string (N.repr_dirpath dirpath) in
+  token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)]
 
 let token_list_of_kernel_name tag =
  let module N = Names in
@@ -202,7 +202,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Errors.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
+          Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -455,8 +455,8 @@ print_endline "PASSATO" ; flush stdout ;
                 let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in
                 let he1'' =
                  String.concat "/"
-                  (List.map Names.string_of_id (List.rev he1')) ^ "/"
-                 ^ (Names.string_of_id he1_id) ^ ".var"
+                  (List.map Names.Id.to_string (List.rev he1')) ^ "/"
+                 ^ (Names.Id.to_string he1_id) ^ ".var"
                 in
                  (he1'',he2)::subst, extra_args, uninst
            in
@@ -501,13 +501,13 @@ print_endline "PASSATO" ; flush stdout ;
                A.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
            | T.Var id ->
 	      let pvars = Termops.ids_of_named_context (E.named_context env) in
-	      let pvars = List.map N.string_of_id pvars in
-              let path = get_uri_of_var (N.string_of_id id) pvars in
+	      let pvars = List.map N.Id.to_string pvars in
+              let path = get_uri_of_var (N.Id.to_string id) pvars in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
                 add_inner_type fresh_id'' ;
                A.AVar
-                (fresh_id'', path ^ "/" ^ (N.string_of_id id) ^ ".var")
+                (fresh_id'', path ^ "/" ^ (N.Id.to_string id) ^ ".var")
            | T.Evar (n,l) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
@@ -610,7 +610,7 @@ print_endline "PASSATO" ; flush stdout ;
            | T.LetIn (n,s,t,d) ->
               let id =
                match n with
-                   N.Anonymous -> N.id_of_string "_X"
+                   N.Anonymous -> N.Id.of_string "_X"
                  | N.Name id -> id
               in
               let n' =
@@ -886,7 +886,7 @@ let acic_object_of_cic_object sigma obj =
                          in
                          let dummy_never_used =
                           let s = "dummy_never_used" in
-                           A.ARel (s,99,s,Names.id_of_string s)
+                           A.ARel (s,99,s,Names.Id.of_string s)
                          in
                           final_env,final_idrefs,
                            (hid,(n,A.Def (at,dummy_never_used)))::atl
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 8259266af..35760a51d 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -35,7 +35,7 @@ let filter_params pvars hyps =
       let ids' = id::ids in
       let ids'' =
        "cic:/" ^
-        String.concat "/" (List.rev (List.map Names.string_of_id ids')) in
+        String.concat "/" (List.rev (List.map Names.Id.to_string ids')) in
       let he' =
        ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in
       let tl' = aux ids' tl in
@@ -44,7 +44,7 @@ let filter_params pvars hyps =
         | _,_  -> he'::tl'
  in
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    aux (Names.repr_dirpath modulepath) (List.rev pvars)
 ;;
@@ -55,7 +55,7 @@ let filter_params pvars hyps =
 let search_variables () =
  let module N = Names in
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    let rec aux =
     function
@@ -63,7 +63,7 @@ let search_variables () =
      | he::tl as modules ->
         let one_section_variables =
          let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
-          let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in
+          let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in
            [he,t]
         in
          one_section_variables @ aux tl
@@ -113,7 +113,7 @@ let theory_filename xml_library_root =
   match xml_library_root with
     None -> None  (* stdout *)
   | Some xml_library_root' ->
-     let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
+     let toks = List.map N.Id.to_string (N.repr_dirpath (Lib.library_dp ())) in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -153,7 +153,7 @@ let print_object uri obj sigma filename =
 
 let string_list_of_named_context_list =
  List.map
-  (function (n,_,_) -> Names.string_of_id n)
+  (function (n,_,_) -> Names.Id.to_string n)
 ;;
 
 (* Function to collect the variables that occur in a term. *)
@@ -212,11 +212,11 @@ let mk_variable_obj id body typ =
    | Some bo -> find_hyps bo, Some (Unshare.unshare bo)
  in
   let hyps' = find_hyps typ @ hyps in
-  let hyps'' = List.map Names.string_of_id hyps' in
+  let hyps'' = List.map Names.Id.to_string hyps' in
   let variables = search_variables () in
   let params = filter_params variables hyps'' in
    Acic.Variable
-    (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params)
+    (Names.Id.to_string id, unsharedbody, Unshare.unshare typ, params)
 ;;
 
 
@@ -226,10 +226,10 @@ let mk_constant_obj id bo ty variables hyps =
  let params = filter_params variables hyps in
   match bo with
      None ->
-      Acic.Constant (Names.string_of_id id,None,ty,params)
+      Acic.Constant (Names.Id.to_string id,None,ty,params)
    | Some c ->
       Acic.Constant
-       (Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)),
+       (Names.Id.to_string id, Some (Unshare.unshare (Declarations.force c)),
          ty,params)
 ;;
 
@@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
-    (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir)))
+    (List.map Names.Id.to_string (List.rev (Names.repr_dirpath dir)))
 ;;
 
 let _ =