Modulification of identifier

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

35 files changed, 296 insertions, 296 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index ecc0930c1..7ac79356f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -152,7 +152,7 @@ let lookup_tacs (hdc,c) st (l,l',dn) =
 module Constr_map = Map.Make(RefOrdered)
 
 let is_transparent_gr (ids, csts) = function
-  | VarRef id -> Idpred.mem id ids
+  | VarRef id -> Id.Pred.mem id ids
   | ConstRef cst -> Cpred.mem cst csts
   | IndRef _ | ConstructRef _ -> false
 
@@ -308,7 +308,7 @@ module Hint_db = struct
   type t = {
     hintdb_state : Names.transparent_state;
     hintdb_cut : hints_path;
-    hintdb_unfolds : Idset.t * Cset.t;
+    hintdb_unfolds : Id.Set.t * Cset.t;
     mutable hintdb_max_id : int;
     use_dn : bool;
     hintdb_map : search_entry Constr_map.t;
@@ -322,7 +322,7 @@ module Hint_db = struct
 
   let empty st use_dn = { hintdb_state = st;
 			  hintdb_cut = PathEmpty;
-			  hintdb_unfolds = (Idset.empty, Cset.empty);
+			  hintdb_unfolds = (Id.Set.empty, Cset.empty);
 			  hintdb_max_id = 0;
 			  use_dn = use_dn;
 			  hintdb_map = Constr_map.empty;
@@ -384,7 +384,7 @@ module Hint_db = struct
       | Unfold_nth egr ->
 	  let addunf (ids,csts) (ids',csts') =
 	    match egr with
-	    | EvalVarRef id -> (Idpred.add id ids, csts), (Idset.add id ids', csts')
+	    | EvalVarRef id -> (Id.Pred.add id ids, csts), (Id.Set.add id ids', csts')
 	    | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts')
 	  in 
 	  let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in
@@ -611,7 +611,7 @@ let add_transparency dbname grs b =
     List.fold_left (fun (ids, csts) gr ->
       match gr with
       | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts)
-      | EvalVarRef v -> (if b then Idpred.add else Idpred.remove) v ids, csts)
+      | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts)
       st grs
   in searchtable_add (dbname, Hint_db.set_transparent_state db st')
 
@@ -806,7 +806,7 @@ type hints_entry =
   | HintsExternEntry of
       int * (patvar list * constr_pattern) option * glob_tactic_expr
 
-let h = id_of_string "H"
+let h = Id.of_string "H"
 
 exception Found of constr * types
 
@@ -833,8 +833,8 @@ let prepare_hint env (sigma,c) =
   let rec iter c =
     try find_next_evar c; c
     with Found (evar,t) ->
-      let id = next_ident_away_from h (fun id -> Idset.mem id !vars) in
-      vars := Idset.add id !vars;
+      let id = next_ident_away_from h (fun id -> Id.Set.mem id !vars) in
+      vars := Id.Set.add id !vars;
       subst := (evar,mkVar id)::!subst;
       mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in
   iter c
@@ -1312,7 +1312,7 @@ and my_find_search_delta db_list local_db hdc concl =
 	    let l =
 	      match hdc with None -> Hint_db.map_none db
 	      | Some hdc ->
-		  if (Idpred.is_empty ids && Cpred.is_empty csts)
+		  if (Id.Pred.is_empty ids && Cpred.is_empty csts)
 		  then Hint_db.map_auto (hdc,concl) db
 		  else Hint_db.map_all hdc db
 	    in {flags with modulo_delta = st}, l
diff --git a/tactics/auto.mli b/tactics/auto.mli
index b7f5a312a..2ec0c877d 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -88,7 +88,7 @@ module Hint_db :
     val add_cut : hints_path -> t -> t
     val cut : t -> hints_path
 
-    val unfolds : t -> Idset.t * Cset.t
+    val unfolds : t -> Id.Set.t * Cset.t
   end
 
 type hint_db_name = string
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 672b5bc45..cae417ad3 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -129,7 +129,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic =
      match Tacmach.pf_hyps gl with
         (last_hyp_id,_,_)::_ -> last_hyp_id
       | _ -> (* even the hypothesis id is missing *)
-             error ("No such hypothesis: " ^ (string_of_id !id) ^".")
+             error ("No such hypothesis: " ^ (Id.to_string !id) ^".")
     in
     let gl' = general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false gl in
     let gls = gl'.Evd.it in
@@ -137,7 +137,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic =
        g::_ ->
         (match Environ.named_context_of_val (Goal.V82.hyps gl'.Evd.sigma g) with
             (lastid,_,_)::_ ->
-              if not (id_eq last_hyp_id lastid) then
+              if not (Id.equal last_hyp_id lastid) then
                begin
                 let gl'' =
                   if !to_be_cleared then
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index ab335f789..773e3694e 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -22,7 +22,7 @@ val add_rew_rules : string -> raw_rew_rule list -> unit
    Default is Naive: first match in the clause, don't look at the side-conditions to
    tell if the rewrite succeeded. *)
 val autorewrite : ?conds:conditions -> tactic -> string list -> tactic
-val autorewrite_in : ?conds:conditions -> Names.identifier -> tactic -> string list -> tactic
+val autorewrite_in : ?conds:conditions -> Names.Id.t -> tactic -> string list -> tactic
 
 (** Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 875370501..0a1845322 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -74,7 +74,7 @@ struct
       | Const c -> if Cpred.mem c cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l)
       | Ind ind_sp -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l)
       | Construct cstr_sp -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l)
-      | Var id when not (Idpred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
+      | Var id when not (Id.Pred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l)
       | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c])
       | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l)
       | Sort _ -> Dn.Label(Term_dn.SortLabel, [])
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 4d037843e..f1297647c 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -449,7 +449,7 @@ let autounfolds db occs =
     in
     let (ids, csts) = Hint_db.unfolds db in
       Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
-	(Idset.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
+	(Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
   in unfold_option unfolds
 
 let autounfold db cls gl =
@@ -471,7 +471,7 @@ END
 let unfold_head env (ids, csts) c = 
   let rec aux c = 
     match kind_of_term c with
-    | Var id when Idset.mem id ids ->
+    | Var id when Id.Set.mem id ids ->
 	(match Environ.named_body id env with
 	| Some b -> true, b
 	| None -> false, c)
@@ -507,7 +507,7 @@ let autounfold_one db cl gl =
 	with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
       in
       let (ids, csts) = Hint_db.unfolds db in
-	(Idset.union ids i, Cset.union csts c)) (Idset.empty, Cset.empty) db
+	(Id.Set.union ids i, Cset.union csts c)) (Id.Set.empty, Cset.empty) db
   in
   let did, c' = unfold_head (pf_env gl) st (match cl with Some (id, _) -> pf_get_hyp_typ gl id | None -> pf_concl gl) in
     if did then
@@ -517,7 +517,7 @@ let autounfold_one db cl gl =
     else tclFAIL 0 (str "Nothing to unfold") gl
 
 (* 	  Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts *)
-(* 	    (Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
+(* 	    (Id.Set.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db) *)
 (*       in unfold_option unfolds cl *)
 
 (*       let db = try searchtable_map dbname  *)
@@ -525,7 +525,7 @@ let autounfold_one db cl gl =
 (*       in *)
 (*       let (ids, csts) = Hint_db.unfolds db in *)
 (* 	Cset.fold (fun cst -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cst)) csts *)
-(* 	  (Idset.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *)
+(* 	  (Id.Set.fold (fun id -> tclORELSE (unfold_option [(occ, EvalVarRef id)] cl) ids acc))) *)
 (*       (tclFAIL 0 (mt())) db *)
       
 TACTIC EXTEND autounfold_one
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 88348206b..faa32ab86 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -81,7 +81,7 @@ and general_decompose_aux recognizer id =
    pas si aucune élimination n'est possible *)
 
 (* Meilleures stratégies mais perte de compatibilité *)
-let tmphyp_name = id_of_string "_TmpHyp"
+let tmphyp_name = Id.of_string "_TmpHyp"
 let up_to_delta = ref false (* true *)
 
 let general_decompose recognizer c gl =
diff --git a/tactics/elim.mli b/tactics/elim.mli
index a1af31c6b..d135997cd 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -23,7 +23,7 @@ val introCaseAssumsThen :
   (intro_pattern_expr Loc.located list -> branch_assumptions -> tactic) ->
     branch_args -> tactic
 
-val general_decompose : (identifier * constr -> bool) -> constr -> tactic
+val general_decompose : (Id.t * constr -> bool) -> constr -> tactic
 val decompose_nonrec  : constr -> tactic
 val decompose_and     : constr -> tactic
 val decompose_or      : constr -> tactic
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 6500b0e53..a5f8831a0 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -85,8 +85,8 @@ let mkDecideEqGoal eqonleft op rectype c1 c2 g =
 
 let mkGenDecideEqGoal rectype g =
   let hypnames = pf_ids_of_hyps g in
-  let xname    = next_ident_away (id_of_string "x") hypnames
-  and yname    = next_ident_away (id_of_string "y") hypnames in
+  let xname    = next_ident_away (Id.of_string "x") hypnames
+  and yname    = next_ident_away (Id.of_string "y") hypnames in
   (mkNamedProd xname rectype
      (mkNamedProd yname rectype
         (mkDecideEqGoal true (build_coq_sumbool ())
@@ -99,8 +99,8 @@ let eqCase tac =
   tac)))
 
 let diseqCase eqonleft =
-  let diseq  = id_of_string "diseq" in
-  let absurd = id_of_string "absurd" in
+  let diseq  = Id.of_string "diseq" in
+  let absurd = Id.of_string "absurd" in
   (tclTHEN (intro_using diseq)
   (tclTHEN (choose_noteq eqonleft)
   (tclTHEN  red_in_concl
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 5f6c776ba..27d086095 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -57,8 +57,8 @@ open Inductiveops
 open Ind_tables
 open Indrec
 
-let hid = id_of_string "H"
-let xid = id_of_string "X"
+let hid = Id.of_string "H"
+let xid = Id.of_string "X"
 let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
 let fresh env id = next_global_ident_away id []
 
@@ -311,8 +311,8 @@ let build_l2r_rew_scheme dep env ind kind =
       Array.concat [extended_rel_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let varHC = fresh env (id_of_string "HC") in
-  let varP = fresh env (id_of_string "P") in
+  let varHC = fresh env (Id.of_string "HC") in
+  let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive ind specif in
   let applied_ind_P =
     mkApp (mkInd ind, Array.concat
@@ -418,8 +418,8 @@ let build_l2r_forward_rew_scheme dep env ind kind =
       Array.concat [extended_rel_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let varHC = fresh env (id_of_string "HC") in
-  let varP = fresh env (id_of_string "P") in
+  let varHC = fresh env (Id.of_string "HC") in
+  let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive ind specif in
   let applied_ind_P =
     mkApp (mkInd ind, Array.concat
@@ -504,8 +504,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
     mkApp (mkConstruct(ind,1),extended_rel_vect n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let varHC = fresh env (id_of_string "HC") in
-  let varP = fresh env (id_of_string "P") in
+  let varHC = fresh env (Id.of_string "HC") in
+  let varP = fresh env (Id.of_string "P") in
   let applied_ind = build_dependent_inductive ind specif in
   let realsign_ind =
     name_context env ((Name varH,None,applied_ind)::realsign) in
@@ -691,9 +691,9 @@ let build_congr env (eq,refl) ind =
   if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
-  let varB = fresh env (id_of_string "B") in
-  let varH = fresh env (id_of_string "H") in
-  let varf = fresh env (id_of_string "f") in
+  let varB = fresh env (Id.of_string "B") in
+  let varH = fresh env (Id.of_string "H") in
+  let varf = fresh env (Id.of_string "f") in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   my_it_mkLambda_or_LetIn mib.mind_params_ctxt
      (mkNamedLambda varB (new_Type ())
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8d457d9f4..1af172bfb 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -399,7 +399,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  (* If the term to rewrite uses an hypothesis H, don't rewrite in H *)
 	  let ids =
 	    let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in
-	      Idset.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl)
+	      Id.Set.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in
 	if cl.concl_occs == NoOccurrences then do_hyps else
@@ -755,7 +755,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq =
   let eq_elim     = ind_scheme_of_eq lbeq in
   (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term)
 
-let eq_baseid = id_of_string "e"
+let eq_baseid = Id.of_string "e"
 
 let apply_on_clause (f,t) clause =
   let sigma =  clause.evd in
@@ -1140,7 +1140,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause =
               then (
 (* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*)
               let qidl = qualid_of_reference
-                (Ident (Loc.ghost,id_of_string "Eqdep_dec")) in
+                (Ident (Loc.ghost,Id.of_string "Eqdep_dec")) in
               Library.require_library [qidl] (Some false);
 (* cut with the good equality and prove the requested goal *)
               tclTHENS (cut (mkApp (ceq,new_eq_args)) )
@@ -1394,7 +1394,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *)
     not (eq_constr eq (constr_of_global glob_identity)) then
     raise PatternMatchingFailure
 
-exception FoundHyp of (identifier * constr * bool)
+exception FoundHyp of (Id.t * constr * bool)
 
 (* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *)
 let is_eq_x gl x (id,_,c) =
@@ -1412,7 +1412,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
   (* The set of hypotheses using x *)
   let depdecls =
     let test (id,_,c as dcl) =
-      if not (id_eq id hyp) && occur_var_in_decl (pf_env gl) x dcl then Some dcl
+      if not (Id.equal id hyp) && occur_var_in_decl (pf_env gl) x dcl then Some dcl
       else None in
     List.rev (List.map_filter test (pf_hyps gl)) in
   let dephyps = List.map (fun (id,_,_) -> id) depdecls in
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 7b93727ce..ddef64502 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -52,21 +52,21 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr  -> tactic
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
 val register_general_rewrite_clause :
-  (identifier option -> orientation ->
+  (Id.t option -> orientation ->
     occurrences -> constr with_bindings -> new_goals:constr list -> tactic) -> unit
 val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit
 
-val general_rewrite_ebindings_clause : identifier option ->
+val general_rewrite_ebindings_clause : Id.t option ->
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
   ?tac:(tactic * conditions) -> constr with_bindings -> evars_flag -> tactic
 
 val general_rewrite_bindings_in :
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
   ?tac:(tactic * conditions) ->
-  identifier -> constr with_bindings -> evars_flag -> tactic
+  Id.t -> constr with_bindings -> evars_flag -> tactic
 val general_rewrite_in          :
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag -> 
-  ?tac:(tactic * conditions) -> identifier -> constr -> evars_flag -> tactic
+  ?tac:(tactic * conditions) -> Id.t -> constr -> evars_flag -> tactic
 
 val general_multi_rewrite :
   orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic
@@ -80,14 +80,14 @@ val general_multi_multi_rewrite :
 
 val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
 val replace    : constr -> constr -> tactic
-val replace_in : identifier -> constr -> constr -> tactic
+val replace_in : Id.t -> constr -> constr -> tactic
 val replace_by : constr -> constr -> tactic -> tactic
-val replace_in_by : identifier -> constr -> constr -> tactic -> tactic
+val replace_in_by : Id.t -> constr -> constr -> tactic -> tactic
 
 val discr        : evars_flag -> constr with_bindings -> tactic
 val discrConcl   : tactic
 val discrClause  : evars_flag -> clause -> tactic
-val discrHyp     : identifier -> tactic
+val discrHyp     : Id.t -> tactic
 val discrEverywhere : evars_flag -> tactic
 val discr_tac    : evars_flag ->
   constr with_bindings induction_arg option -> tactic
@@ -95,7 +95,7 @@ val inj          : intro_pattern_expr Loc.located list -> evars_flag ->
   constr with_bindings -> tactic
 val injClause    : intro_pattern_expr Loc.located list -> evars_flag ->
   constr with_bindings induction_arg option -> tactic
-val injHyp       : identifier -> tactic
+val injHyp       : Id.t -> tactic
 val injConcl     : tactic
 
 val dEq : evars_flag -> constr with_bindings induction_arg option -> tactic
@@ -105,29 +105,29 @@ val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
 
 (* The family cutRewriteIn expect an equality statement *)
-val cutRewriteInHyp : bool -> types -> identifier -> tactic
+val cutRewriteInHyp : bool -> types -> Id.t -> tactic
 val cutRewriteInConcl : bool -> constr -> tactic
 
 (* The family rewriteIn expect the proof of an equality *)
-val rewriteInHyp : bool -> constr -> identifier -> tactic
+val rewriteInHyp : bool -> constr -> Id.t -> tactic
 val rewriteInConcl : bool -> constr -> tactic
 
 (* Expect the proof of an equality; fails with raw internal errors *)
-val substClause : bool -> constr -> identifier option -> tactic
+val substClause : bool -> constr -> Id.t option -> tactic
 
 val discriminable : env -> evar_map -> constr -> constr -> bool
 val injectable : env -> evar_map -> constr -> constr -> bool
 
 (* Subst *)
 
-val unfold_body : identifier -> tactic
+val unfold_body : Id.t -> tactic
 
 type subst_tactic_flags = {
   only_leibniz : bool;
   rewrite_dependent_proof : bool
 }
-val subst_gen : bool -> identifier list -> tactic
-val subst : identifier list -> tactic
+val subst_gen : bool -> Id.t list -> tactic
+val subst : Id.t list -> tactic
 val subst_all : ?flags:subst_tactic_flags -> tactic
 
 (* Replace term *)
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 9220a60bd..7813f5326 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -12,6 +12,6 @@ open Tacexpr
 open Locus
 
 val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
-  (identifier * hyp_location_flag, unit) location -> tactic
+  (Id.t * hyp_location_flag, unit) location -> tactic
 
 val let_evar : name -> Term.types -> tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 5c2746986..a15f907c6 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -121,8 +121,8 @@ END
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
 
-type loc_place = identifier Loc.located gen_place
-type place = identifier gen_place
+type loc_place = Id.t Loc.located gen_place
+type place = Id.t gen_place
 
 let pr_gen_place pr_id = function
     ConclLocation () -> Pp.mt ()
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 31f51866f..7fc3ac8a5 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -33,21 +33,21 @@ val glob : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 
-type loc_place = identifier Loc.located gen_place
-type place = identifier gen_place
+type loc_place = Id.t Loc.located gen_place
+type place = Id.t gen_place
 
 val rawwit_hloc : loc_place raw_abstract_argument_type
 val wit_hloc : place typed_abstract_argument_type
 val hloc : loc_place Pcoq.Gram.entry
 val pr_hloc : loc_place -> Pp.std_ppcmds
 
-val in_arg_hyp:  (Names.identifier Loc.located list option * bool)  Pcoq.Gram.entry
-val globwit_in_arg_hyp : (Names.identifier Loc.located list option * bool) glob_abstract_argument_type
-val rawwit_in_arg_hyp : (Names.identifier Loc.located list option * bool) raw_abstract_argument_type
-val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
-val raw_in_arg_hyp_to_clause : (Names.identifier Loc.located list option * bool) -> Locus.clause
-val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Locus.clause
-val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds
+val in_arg_hyp:  (Names.Id.t Loc.located list option * bool)  Pcoq.Gram.entry
+val globwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) glob_abstract_argument_type
+val rawwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) raw_abstract_argument_type
+val wit_in_arg_hyp : (Names.Id.t list option * bool) typed_abstract_argument_type
+val raw_in_arg_hyp_to_clause : (Names.Id.t Loc.located list option * bool) -> Locus.clause
+val glob_in_arg_hyp_to_clause :  (Names.Id.t list option * bool)  -> Locus.clause
+val pr_in_arg_hyp : (Names.Id.t list option * bool) -> Pp.std_ppcmds
 
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
 val rawwit_by_arg_tac :  raw_tactic_expr option raw_abstract_argument_type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ade53e768..2cfec1e21 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -551,7 +551,7 @@ let subst_var_with_hole occ tid t =
   let locref = ref 0 in
   let rec substrec = function
     | GVar (_,id) as x -> 
-        if id_eq id tid 
+        if Id.equal id tid 
         then
 	  (decr occref;
 	   if Int.equal !occref 0 then x
@@ -650,7 +650,7 @@ END
 exception Found of tactic
 
 let rewrite_except h g =
-  tclMAP (fun id -> if id_eq id h then tclIDTAC else 
+  tclMAP (fun id -> if Id.equal id h then tclIDTAC else 
       tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
     (Tacmach.pf_ids_of_hyps g) g
 
@@ -684,7 +684,7 @@ let case_eq_intros_rewrite x g =
       mkCaseEq x;
       (fun g -> 
 	let n' = nb_prod (Tacmach.pf_concl g) in
-	let h = fresh_id (Tacmach.pf_ids_of_hyps g) (id_of_string "heq") g in
+	let h = fresh_id (Tacmach.pf_ids_of_hyps g) (Id.of_string "heq") g in
 	tclTHENLIST [ (tclDO (n'-n-1) intro);
 		      Tacmach.introduction h;
 		      rewrite_except h] g
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index ad72a4aac..306067ff0 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -8,8 +8,8 @@
 
 open Proof_type
 
-val discrHyp : Names.identifier -> tactic
-val injHyp : Names.identifier -> tactic
+val discrHyp : Names.Id.t -> tactic
+val injHyp : Names.Id.t -> tactic
 
 val refine_tac : Evd.open_constr -> tactic
 
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 1199fe7a8..47fd9aac2 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -25,8 +25,8 @@ open Misctypes
 
 (** Basic tactics *)
 
-val h_intro_move      : identifier option -> identifier move_location -> tactic
-val h_intro           : identifier -> tactic
+val h_intro_move      : Id.t option -> Id.t move_location -> tactic
+val h_intro           : Id.t -> tactic
 val h_intros_until    : quantified_hypothesis -> tactic
 
 val h_assumption      : tactic
@@ -38,7 +38,7 @@ val h_apply           : advanced_flag -> evars_flag ->
   constr with_bindings located list -> tactic
 val h_apply_in        : advanced_flag -> evars_flag ->
   constr with_bindings located list ->
-  identifier * intro_pattern_expr located option -> tactic
+  Id.t * intro_pattern_expr located option -> tactic
 
 val h_elim            : evars_flag -> constr with_bindings ->
                         constr with_bindings option -> tactic
@@ -46,11 +46,11 @@ val h_elim_type       : constr -> tactic
 val h_case            : evars_flag -> constr with_bindings -> tactic
 val h_case_type       : constr -> tactic
 
-val h_mutual_fix      : identifier -> int ->
-                        (identifier * int * constr) list -> tactic
-val h_fix             : identifier option -> int -> tactic
-val h_mutual_cofix    : identifier -> (identifier * constr) list -> tactic
-val h_cofix           : identifier option -> tactic
+val h_mutual_fix      : Id.t -> int ->
+                        (Id.t * int * constr) list -> tactic
+val h_fix             : Id.t option -> int -> tactic
+val h_mutual_cofix    : Id.t -> (Id.t * constr) list -> tactic
+val h_cofix           : Id.t option -> tactic
 
 val h_cut             : constr -> tactic
 val h_generalize      : constr list -> tactic
@@ -90,11 +90,11 @@ val h_lapply          : constr -> tactic
 
 
 (** Context management *)
-val h_clear           : bool -> identifier list -> tactic
-val h_clear_body      : identifier list -> tactic
-val h_move            : bool -> identifier -> identifier move_location -> tactic
-val h_rename          : (identifier*identifier) list -> tactic
-val h_revert          : identifier list -> tactic
+val h_clear           : bool -> Id.t list -> tactic
+val h_clear_body      : Id.t list -> tactic
+val h_move            : bool -> Id.t -> Id.t move_location -> tactic
+val h_rename          : (Id.t*Id.t) list -> tactic
+val h_revert          : Id.t list -> tactic
 
 (** Constructors *)
 val h_constructor     : evars_flag -> int -> constr bindings -> tactic
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 65f0e0302..b873c2050 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -288,7 +288,7 @@ let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
 let match_arrow_pattern t =
   match matches coq_arrow_pattern t with
     | [(m1,arg);(m2,mind)] ->
-      assert (id_eq m1 meta1 && id_eq m2 meta2); (arg, mind)
+      assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
     | _ -> anomaly "Incorrect pattern matching"
 
 let match_with_nottype t =
@@ -368,10 +368,10 @@ let match_eq eqn eq_pat =
   let pat = try Lazy.force eq_pat with _ -> raise PatternMatchingFailure in
   match matches pat eqn with
     | [(m1,t);(m2,x);(m3,y)] ->
-	assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3);
+	assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	PolymorphicLeibnizEq (t,x,y)
     | [(m1,t);(m2,x);(m3,t');(m4,x')] ->
-        assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3 && id_eq m4 meta4);
+        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
 	HeterogenousEq (t,x,t',x')
     | _ -> anomaly "match_eq: an eq pattern should match 3 or 4 terms"
 
@@ -412,7 +412,7 @@ open Tacmach
 let match_eq_nf gls eqn eq_pat =
   match pf_matches gls (Lazy.force eq_pat) eqn with
     | [(m1,t);(m2,x);(m3,y)] ->
-        assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3);
+        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3);
 	(t,pf_whd_betadeltaiota gls x,pf_whd_betadeltaiota gls y)
     | _ -> anomaly "match_eq: an eq pattern should match 3 terms"
 
@@ -432,7 +432,7 @@ let coq_exist_pattern = coq_ex_pattern_gen coq_exist_ref
 let match_sigma ex ex_pat =
   match matches (Lazy.force ex_pat) ex with
     | [(m1,a);(m2,p);(m3,car);(m4,cdr)] ->
-        assert (id_eq m1 meta1 && id_eq m2 meta2 && id_eq m3 meta3 && id_eq m4 meta4);
+        assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3 && Id.equal m4 meta4);
 	(a,p,car,cdr)
     | _ ->
 	anomaly "match_sigma: a successful sigma pattern should match 4 terms"
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 1e2d6fa6a..a4f7b5e3f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -448,7 +448,7 @@ let raw_inversion inv_kind id status names gl =
     try pf_reduce_to_atomic_ind gl (pf_type_of gl c)
     with UserError _ ->
       errorlabstrm "raw_inversion"
-	(str ("The type of "^(string_of_id id)^" is not inductive.")) in
+	(str ("The type of "^(Id.to_string id)^" is not inductive.")) in
   let indclause = mk_clenv_from gl (c,t) in
   let ccl = clenv_type indclause in
   check_no_metas indclause ccl;
diff --git a/tactics/inv.mli b/tactics/inv.mli
index 1266ac9f8..52db199ee 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -21,11 +21,11 @@ val inv_gen :
   bool -> inversion_kind -> inversion_status ->
     intro_pattern_expr located option -> quantified_hypothesis -> tactic
 val invIn_gen :
-  inversion_kind -> intro_pattern_expr located option -> identifier list ->
+  inversion_kind -> intro_pattern_expr located option -> Id.t list ->
     quantified_hypothesis -> tactic
 
 val inv_clause :
-  inversion_kind -> intro_pattern_expr located option -> identifier list ->
+  inversion_kind -> intro_pattern_expr located option -> Id.t list ->
     quantified_hypothesis -> tactic
 
 val inv : inversion_kind -> intro_pattern_expr located option ->
@@ -34,9 +34,9 @@ val inv : inversion_kind -> intro_pattern_expr located option ->
 val dinv : inversion_kind -> constr option ->
   intro_pattern_expr located option -> quantified_hypothesis -> tactic
 
-val half_inv_tac : identifier -> tactic
-val inv_tac : identifier -> tactic
-val inv_clear_tac : identifier -> tactic
-val half_dinv_tac : identifier -> tactic
-val dinv_tac : identifier -> tactic
-val dinv_clear_tac : identifier -> tactic
+val half_inv_tac : Id.t -> tactic
+val inv_tac : Id.t -> tactic
+val inv_clear_tac : Id.t -> tactic
+val half_dinv_tac : Id.t -> tactic
+val dinv_tac : Id.t -> tactic
+val dinv_clear_tac : Id.t -> tactic
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 3031734fb..fa2931c80 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -140,7 +140,7 @@ let rec add_prods_sign env sigma t =
 let compute_first_inversion_scheme env sigma ind sort dep_option =
   let indf,realargs = dest_ind_type ind in
   let allvars = ids_of_context env in
-  let p = next_ident_away (id_of_string "P") allvars in
+  let p = next_ident_away (Id.of_string "P") allvars in
   let pty,goal =
     if dep_option  then
       let pty = make_arity env true indf sort in
@@ -210,7 +210,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
   let rec fill_holes c =
     match kind_of_term c with
     | Evar (e,args) ->
-	let h = next_ident_away (id_of_string "H") !avoid in
+	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := h::!avoid;
 	ownSign := add_named_decl (h,None,ty) !ownSign;
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index 45538690c..5019ceda5 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -16,14 +16,14 @@ open Constrexpr
 open Misctypes
 
 val lemInv_gen : quantified_hypothesis -> constr -> tactic
-val lemInvIn_gen : quantified_hypothesis -> constr -> identifier list -> tactic
+val lemInvIn_gen : quantified_hypothesis -> constr -> Id.t list -> tactic
 
 val lemInv_clause :
-  quantified_hypothesis -> constr -> identifier list -> tactic
+  quantified_hypothesis -> constr -> Id.t list -> tactic
 
 val inversion_lemma_from_goal :
-  int -> identifier -> identifier located -> sorts -> bool ->
-    (identifier -> tactic) -> unit
+  int -> Id.t -> Id.t located -> sorts -> bool ->
+    (Id.t -> tactic) -> unit
 val add_inversion_lemma_exn :
-  identifier -> constr_expr -> glob_sort -> bool -> (identifier -> tactic) ->
+  Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> tactic) ->
     unit
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 3d1e4f010..160bcfc70 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -127,7 +127,7 @@ let replace_in_array keep_length env sigma a =
   v',mm,sgp
 
 let fresh env n =
-  let id = match n with Name x -> x | _ -> id_of_string "_H" in
+  let id = match n with Name x -> x | _ -> Id.of_string "_H" in
   next_ident_away_in_goal id (ids_of_named_context (named_context env))
 
 let rec compute_metamap env sigma c = match kind_of_term c with
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index d1eda3f7e..e5fddfde2 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -38,7 +38,7 @@ open Decl_kinds
 (** Typeclass-based generalized rewriting. *)
 
 let classes_dirpath =
-  make_dirpath (List.map id_of_string ["Classes";"Coq"])
+  make_dirpath (List.map Id.of_string ["Classes";"Coq"])
 
 let init_setoid () =
   if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
@@ -52,10 +52,10 @@ let proper_proxy_class =
 
 let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
 
-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 try_find_global_reference dir s =
-  let sp = Libnames.make_path (make_dir ("Coq"::dir)) (id_of_string s) in
+  let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in
     Nametab.global_of_path sp
 
 let try_find_reference dir s =
@@ -229,8 +229,8 @@ let rec decompose_app_rel env evd t =
       else 
 	let (f', args) = decompose_app_rel env evd args.(0) in
 	let ty = Typing.type_of env evd args.(0) in
-	let f'' = mkLambda (Name (id_of_string "x"), ty,
-	  mkLambda (Name (id_of_string "y"), lift 1 ty,
+	let f'' = mkLambda (Name (Id.of_string "x"), ty,
+	  mkLambda (Name (Id.of_string "y"), lift 1 ty,
 	    mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
 	in (f'', args)
   | _ -> error "The term provided is not an applied relation."
@@ -270,7 +270,7 @@ let decompose_applied_relation_expr env sigma flags (is, (c,l)) left2right =
 
 let rewrite_db = "rewrite"
 
-let conv_transparent_state = (Idpred.empty, Cpred.full)
+let conv_transparent_state = (Id.Pred.empty, Cpred.full)
 
 let _ = 
   Auto.add_auto_init
@@ -543,7 +543,7 @@ type rewrite_result_info = {
 
 type rewrite_result = rewrite_result_info option
 
-type strategy = Environ.env -> identifier list -> constr -> types ->
+type strategy = Environ.env -> Id.t list -> constr -> types ->
   constr option -> evars -> rewrite_result option
 
 let get_rew_rel r = match r.rew_prf with
@@ -588,7 +588,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' cstr evars
     let cl_args = [| appmtype' ; signature ; appm |] in
     let app = mkApp (Lazy.force proper_type, cl_args) in
     let env' = Environ.push_named
-      (id_of_string "do_subrelation", Some (Lazy.force do_subrelation), Lazy.force apply_subrelation)
+      (Id.of_string "do_subrelation", Some (Lazy.force do_subrelation), Lazy.force apply_subrelation)
       env
     in
     let evars, morph = new_cstr_evar evars env' app in
@@ -1150,7 +1150,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 		     match abs with
 		     | None -> p
 		     | Some (t, ty) ->
-			 mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |])
+			 mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |])
 		   in
 		     Some (evars, Some (mkApp (term, [| mkVar id |])), newt)
 	       | RewCast c ->
@@ -1162,7 +1162,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 		   (match abs with
 		    | None -> Some (evars, Some p, newt)
 		    | Some (t, ty) ->
-			let proof = mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) in
+			let proof = mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |]) in
 			  Some (evars, Some proof, newt))
 	       | RewCast c -> Some (evars, None, newt))
 	in Some res
@@ -1232,7 +1232,7 @@ let assert_replacing id newt tac =
        let nc' = 
 	 Environ.fold_named_context
 	   (fun _ (n, b, t as decl) nc' ->
-	      if id_eq n id then (n, b, newt) :: nc'
+	      if Id.equal n id then (n, b, newt) :: nc'
 	      else decl :: nc')
 	   env ~init:[]
        in
@@ -1246,7 +1246,7 @@ let assert_replacing id newt tac =
 		      let inst = 
 			fold_named_context
 			  (fun _ (n, b, t) inst ->
-			     if id_eq n id then ev' :: inst
+			     if Id.equal n id then ev' :: inst
 			     else if Option.is_empty b then mkVar n :: inst else inst)
 			  env ~init:[]
 		      in
@@ -1524,7 +1524,7 @@ TACTIC EXTEND rewrite_strat
 END
 
 let clsubstitute o c =
-  let is_tac id = match fst (fst (snd c)) with GVar (_, id') when id_eq id' id -> true | _ -> false in
+  let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
     Tacticals.onAllHypsAndConcl
       (fun cl ->
 	match cl with
@@ -1570,7 +1570,7 @@ TACTIC EXTEND GenRew
     [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ]
 END
 
-let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,id_of_string s))),l)
+let mkappc s l = CAppExpl (Loc.ghost,(None,(Libnames.Ident (Loc.ghost,Id.of_string s))),l)
 
 let declare_an_instance n s args =
   ((Loc.ghost,Name n), Explicit,
@@ -1586,17 +1586,17 @@ let anew_instance global binders instance fields =
 let declare_instance_refl global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
   in anew_instance global binders instance
-       [(Ident (Loc.ghost,id_of_string "reflexivity"),lemma)]
+       [(Ident (Loc.ghost,Id.of_string "reflexivity"),lemma)]
 
 let declare_instance_sym global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric"
   in anew_instance global binders instance
-       [(Ident (Loc.ghost,id_of_string "symmetry"),lemma)]
+       [(Ident (Loc.ghost,Id.of_string "symmetry"),lemma)]
 
 let declare_instance_trans global binders a aeq n lemma =
   let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive"
   in anew_instance global binders instance
-       [(Ident (Loc.ghost,id_of_string "transitivity"),lemma)]
+       [(Ident (Loc.ghost,Id.of_string "transitivity"),lemma)]
 
 let declare_relation ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
@@ -1620,16 +1620,16 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
 	in ignore(
 	    anew_instance global binders instance
-	      [(Ident (Loc.ghost,id_of_string "PreOrder_Reflexive"), lemma1);
-	       (Ident (Loc.ghost,id_of_string "PreOrder_Transitive"),lemma3)])
+	      [(Ident (Loc.ghost,Id.of_string "PreOrder_Reflexive"), lemma1);
+	       (Ident (Loc.ghost,Id.of_string "PreOrder_Transitive"),lemma3)])
     | (None, Some lemma2, Some lemma3) ->
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
 	let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
 	in ignore(
 	    anew_instance global binders instance
-	      [(Ident (Loc.ghost,id_of_string "PER_Symmetric"), lemma2);
-	       (Ident (Loc.ghost,id_of_string "PER_Transitive"),lemma3)])
+	      [(Ident (Loc.ghost,Id.of_string "PER_Symmetric"), lemma2);
+	       (Ident (Loc.ghost,Id.of_string "PER_Transitive"),lemma3)])
      | (Some lemma1, Some lemma2, Some lemma3) ->
 	let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in
 	let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in
@@ -1637,9 +1637,9 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
 	in ignore(
 	  anew_instance global binders instance
-	    [(Ident (Loc.ghost,id_of_string "Equivalence_Reflexive"), lemma1);
-	     (Ident (Loc.ghost,id_of_string "Equivalence_Symmetric"), lemma2);
-	     (Ident (Loc.ghost,id_of_string "Equivalence_Transitive"), lemma3)])
+	    [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), lemma1);
+	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
+	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
 
 type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
 
@@ -1815,9 +1815,9 @@ let add_setoid global binders a aeq t n =
   let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
   in ignore(
     anew_instance global binders instance
-      [(Ident (Loc.ghost,id_of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
-       (Ident (Loc.ghost,id_of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
-       (Ident (Loc.ghost,id_of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+      [(Ident (Loc.ghost,Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
+       (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
+       (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
 
 let add_morphism_infer glob m n =
   init_setoid ();
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 9a8774b11..0f2ac6cfe 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -53,9 +53,9 @@ let skip_metaid = function
 (** Generic arguments *)
 
 type glob_sign = {
-  ltacvars : identifier list * identifier list;
+  ltacvars : Id.t list * Id.t list;
      (* ltac variables and the subset of vars introduced by Intro/Let/... *)
-  ltacrecvars : (identifier * ltac_constant) list;
+  ltacrecvars : (Id.t * ltac_constant) list;
      (* ltac recursive names *)
   gsigma : Evd.evar_map;
   genv : Environ.env }
@@ -87,10 +87,10 @@ let lookup_intern_genarg id =
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 
-let atomic_mactab = ref Idmap.empty
+let atomic_mactab = ref Id.Map.empty
 let add_primitive_tactic s tac =
-  let id = id_of_string s in
-  atomic_mactab := Idmap.add id tac !atomic_mactab
+  let id = Id.of_string s in
+  atomic_mactab := Id.Map.add id tac !atomic_mactab
 
 let _ =
   let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
@@ -124,10 +124,10 @@ let _ =
         "fresh", TacArg(dloc,TacFreshId [])
       ]
 
-let lookup_atomic id = Idmap.find id !atomic_mactab
+let lookup_atomic id = Id.Map.find id !atomic_mactab
 let is_atomic_kn kn =
   let (_,_,l) = repr_kn kn in
-  Idmap.mem (id_of_label l) !atomic_mactab
+  Id.Map.mem (id_of_label l) !atomic_mactab
 
 (* Tactics table (TacExtend). *)
 
@@ -753,7 +753,7 @@ and intern_tacarg strict onlytac ist = function
   | ConstrMayEval c -> ConstrMayEval (intern_constr_may_eval ist c)
   | MetaIdArg (loc,istac,s) ->
       (* $id can occur in Grammar tactic... *)
-      let id = id_of_string s in
+      let id = Id.of_string s in
       if find_ltacvar id ist then
 	if istac then Reference (ArgVar (adjust_loc loc,id))
 	else ConstrMayEval (ConstrTerm (GVar (adjust_loc loc,id), None))
@@ -865,7 +865,7 @@ let add (kn,td) = mactab := Gmap.add kn td !mactab
 let replace (kn,td) = mactab := Gmap.add kn td (Gmap.remove kn !mactab)
 
 type tacdef_kind =
-  | NewTac of identifier
+  | NewTac of Id.t
   | UpdateTac of ltac_constant
 
 let load_md i ((sp,kn),(local,defs)) =
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 69a708d23..5f302f1b9 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -24,8 +24,8 @@ open Nametab
     Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
 
 type glob_sign = {
-  ltacvars : identifier list * identifier list;
-  ltacrecvars : (identifier * ltac_constant) list;
+  ltacvars : Id.t list * Id.t list;
+  ltacrecvars : (Id.t * ltac_constant) list;
   gsigma : Evd.evar_map;
   genv : Environ.env }
 
@@ -40,7 +40,7 @@ val make_empty_glob_sign : unit -> glob_sign
 val glob_tactic : raw_tactic_expr -> glob_tactic_expr
 
 val glob_tactic_env :
-  identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
+  Id.t list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
 
 (** Low-level variants *)
 
@@ -55,7 +55,7 @@ val intern_constr_with_bindings :
   glob_sign -> constr_expr * constr_expr bindings ->
   glob_constr_and_expr * glob_constr_and_expr bindings
 
-val intern_hyp : glob_sign -> identifier Loc.located -> identifier Loc.located
+val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
 
 (** Adds a globalization function for extra generic arguments *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3f7cbb625..3db2328e2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -53,8 +53,8 @@ let safe_msgnl s =
 type value =
   | VRTactic of (goal list sigma) (* For Match results *)
                                                (* Not a true value *)
-  | VFun of ltac_trace * (identifier*value) list *
-      identifier option list * glob_tactic_expr
+  | VFun of ltac_trace * (Id.t*value) list *
+      Id.t option list * glob_tactic_expr
   | VVoid
   | VInteger of int
   | VIntroPattern of intro_pattern_expr (* includes idents which are not *)
@@ -64,7 +64,7 @@ type value =
                         (* includes idents known to be bound and references *)
   | VConstr_context of constr
   | VList of value list
-  | VRec of (identifier*value) list ref * glob_tactic_expr
+  | VRec of (Id.t*value) list ref * glob_tactic_expr
 
 let dloc = Loc.ghost
 
@@ -83,8 +83,8 @@ let catch_error call_trace tac g =
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
-    { lfun : (identifier * value) list;
-      avoid_ids : identifier list; (* ids inherited from the call context
+    { lfun : (Id.t * value) list;
+      avoid_ids : Id.t list; (* ids inherited from the call context
 				      (needed to get fresh ids) *)
       debug : debug_info;
       trace : ltac_trace }
@@ -234,7 +234,7 @@ let try_interp_ltac_var coerce ist env (loc,id) =
 
 let interp_ltac_var coerce ist env locid =
   try try_interp_ltac_var coerce ist env locid
-  with Not_found -> anomaly ("Detected '" ^ (string_of_id (snd locid)) ^ "' as ltac var at interning time")
+  with Not_found -> anomaly ("Detected '" ^ (Id.to_string (snd locid)) ^ "' as ltac var at interning time")
 
 (* Interprets an identifier which must be fresh *)
 let coerce_to_ident fresh env = function
@@ -271,11 +271,11 @@ let interp_intro_pattern_var loc ist env id =
   with Not_found -> IntroIdentifier id
 
 let coerce_to_hint_base = function
-  | VIntroPattern (IntroIdentifier id) -> string_of_id id
+  | VIntroPattern (IntroIdentifier id) -> Id.to_string id
   | _ -> raise (CannotCoerceTo "a hint base name")
 
 let interp_hint_base ist s =
-  try try_interp_ltac_var coerce_to_hint_base ist None (dloc,id_of_string s)
+  try try_interp_ltac_var coerce_to_hint_base ist None (dloc,Id.of_string s)
   with Not_found -> s
 
 let coerce_to_int = function
@@ -438,7 +438,7 @@ let rec extract_ids ids = function
   | _::tl -> extract_ids ids tl
   | [] -> []
 
-let default_fresh_id = id_of_string "H"
+let default_fresh_id = Id.of_string "H"
 
 let interp_fresh_id ist env l =
   let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
@@ -449,9 +449,9 @@ let interp_fresh_id ist env l =
       let s =
 	String.concat "" (List.map (function
 	  | ArgArg s -> s
-	  | ArgVar (_,id) -> string_of_id (interp_ident ist env id)) l) in
+	  | ArgVar (_,id) -> Id.to_string (interp_ident ist env id)) l) in
       let s = if Lexer.is_keyword s then s^"0" else s in
-      id_of_string s in
+      Id.of_string s in
   Tactics.fresh_id_in_env avoid id env
 
 let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl)
@@ -831,7 +831,7 @@ let read_pattern lfun ist env sigma = function
 let cons_and_check_name id l =
   if List.mem id l then
     user_err_loc (dloc,"read_match_goal_hyps",
-      strbrk ("Hypothesis pattern-matching variable "^(string_of_id id)^
+      strbrk ("Hypothesis pattern-matching variable "^(Id.to_string id)^
       " used twice in the same pattern."))
   else id::l
 
@@ -866,7 +866,7 @@ let equal_instances gl (ctx',c') (ctx,c) =
   (* How to compare instances? Do we want the terms to be convertible?
      unifiable? Do we want the universe levels to be relevant? 
      (historically, conv_x is used) *)
-  List.equal id_eq ctx ctx' && pf_conv_x gl c' c
+  List.equal Id.equal ctx ctx' && pf_conv_x gl c' c
 
 (* Verifies if the matched list is coherent with respect to lcm *)
 (* While non-linear matching is modulo eq_constr in matches, merge of *)
@@ -874,7 +874,7 @@ let equal_instances gl (ctx',c') (ctx,c) =
 let verify_metas_coherence gl (ln1,lcm) (ln,lm) =
   let rec aux = function
   | (id,c as x)::tl ->
-      if List.for_all (fun (id',c') -> not (id_eq id' id) || equal_instances gl c' c) lcm
+      if List.for_all (fun (id',c') -> not (Id.equal id' id) || equal_instances gl c' c) lcm
       then
 	x :: aux tl
       else
@@ -1496,13 +1496,13 @@ and interp_ltac_constr ist gl e =
 		    str "instantiated arguments " ++ fnl() ++
                     List.fold_right
                     (fun p s ->
-                      let (i,v) = p in str (string_of_id i) ++ str ", " ++ s)
+                      let (i,v) = p in str (Id.to_string i) ++ str ", " ++ s)
                     il (str "") ++
                     str "uninstantiated arguments " ++ fnl() ++
                     List.fold_right
                     (fun opt_id s ->
                       (match opt_id with
-                          Some id -> str (string_of_id id)
+                          Some id -> str (Id.to_string id)
                         | None -> str "_") ++ str ", " ++ s)
                     ul (mt()))
             | VVoid -> str "VVoid"
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 1401bab4e..eba62f5d7 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -22,20 +22,20 @@ open Misctypes
 (** Values for interpretation *)
 type value =
   | VRTactic of (goal list sigma)
-  | VFun of ltac_trace * (identifier*value) list *
-      identifier option list * glob_tactic_expr
+  | VFun of ltac_trace * (Id.t*value) list *
+      Id.t option list * glob_tactic_expr
   | VVoid
   | VInteger of int
   | VIntroPattern of intro_pattern_expr
   | VConstr of Pattern.constr_under_binders
   | VConstr_context of constr
   | VList of value list
-  | VRec of (identifier*value) list ref * glob_tactic_expr
+  | VRec of (Id.t*value) list ref * glob_tactic_expr
 
 (** Signature for interpretation: val\_interp and interpretation functions *)
 and interp_sign =
-  { lfun : (identifier * value) list;
-    avoid_ids : identifier list;
+  { lfun : (Id.t * value) list;
+    avoid_ids : Id.t list;
     debug : debug_info;
     trace : ltac_trace }
 
@@ -79,7 +79,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map
 
 (** Interprets tactic expressions *)
 
-val interp_hyp :  interp_sign -> goal sigma -> identifier Loc.located -> identifier
+val interp_hyp :  interp_sign -> goal sigma -> Id.t Loc.located -> Id.t
 
 val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
  glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
@@ -93,7 +93,7 @@ val eval_tactic : glob_tactic_expr -> tactic
 
 (** Globalization + interpretation *)
 
-val interp_tac_gen : (identifier * value) list -> identifier list ->
+val interp_tac_gen : (Id.t * value) list -> Id.t list ->
                  debug_info -> raw_tactic_expr -> tactic
 
 val interp : raw_tactic_expr -> tactic
@@ -112,8 +112,8 @@ val declare_xml_printer :
 
 exception CannotCoerceTo of string
 
-val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> identifier Loc.located -> 'a
+val interp_ltac_var : (value -> 'a) -> interp_sign -> Environ.env option -> Id.t Loc.located -> 'a
 
-val interp_int : interp_sign -> identifier Loc.located -> int
+val interp_int : interp_sign -> Id.t Loc.located -> int
 
-val error_ltac_variable : Loc.t -> identifier -> Environ.env option -> value -> string -> 'a
+val error_ltac_variable : Loc.t -> Id.t -> Environ.env option -> value -> string -> 'a
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 68d4890fd..9b32f108c 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -109,7 +109,7 @@ let onNLastHypsId n tac = onHyps (nLastHypsId n) tac
 let onNLastHyps n tac   = onHyps (nLastHyps n) tac
 
 let afterHyp id gl =
-  fst (List.split_when (fun (hyp,_,_) -> id_eq hyp id) (pf_hyps gl))
+  fst (List.split_when (fun (hyp,_,_) -> Id.equal hyp id) (pf_hyps gl))
 
 (***************************************)
 (*           Clause Tacticals          *)
@@ -249,7 +249,7 @@ let general_elim_then_using mk_elim
 	  let name_elim =
 	    match kind_of_term elim with
 	      | Const kn -> string_of_con kn
-	      | Var id -> string_of_id id
+	      | Var id -> Id.to_string id
 	      | _ -> "\b"
 	  in
 	  error ("The elimination combinator " ^ name_elim ^ " is unknown.")
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 61b80b584..1d97e2b94 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -69,28 +69,28 @@ val tclFIRST_PROGRESS_ON : ('a -> tactic) -> 'a list -> tactic
 
 (** {6 Tacticals applying to hypotheses } *)
 
-val onNthHypId       : int -> (identifier -> tactic) -> tactic
+val onNthHypId       : int -> (Id.t -> tactic) -> tactic
 val onNthHyp         : int -> (constr -> tactic) -> tactic
 val onNthDecl        : int -> (named_declaration -> tactic) -> tactic
-val onLastHypId      : (identifier -> tactic) -> tactic
+val onLastHypId      : (Id.t -> tactic) -> tactic
 val onLastHyp        : (constr -> tactic) -> tactic
 val onLastDecl       : (named_declaration -> tactic) -> tactic
-val onNLastHypsId    : int -> (identifier list -> tactic) -> tactic
+val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
 val onNLastHyps      : int -> (constr list -> tactic) -> tactic
 val onNLastDecls     : int -> (named_context -> tactic) -> tactic
 
-val lastHypId   : goal sigma -> identifier
+val lastHypId   : goal sigma -> Id.t
 val lastHyp     : goal sigma -> constr
 val lastDecl    : goal sigma -> named_declaration
-val nLastHypsId : int -> goal sigma -> identifier list
+val nLastHypsId : int -> goal sigma -> Id.t list
 val nLastHyps   : int -> goal sigma -> constr list
 val nLastDecls  : int -> goal sigma -> named_context
 
-val afterHyp    : identifier -> goal sigma -> named_context
+val afterHyp    : Id.t -> goal sigma -> named_context
 
-val ifOnHyp     : (identifier * types -> bool) ->
-                  (identifier -> tactic) -> (identifier -> tactic) ->
-		   identifier -> tactic
+val ifOnHyp     : (Id.t * types -> bool) ->
+                  (Id.t -> tactic) -> (Id.t -> tactic) ->
+		   Id.t -> tactic
 
 val onHyps      : (goal sigma -> named_context) ->
                   (named_context -> tactic) -> tactic
@@ -101,14 +101,14 @@ val onHyps      : (goal sigma -> named_context) ->
    goal; in particular, it can abstractly refer to the set of
    hypotheses independently of the effective contents of the current goal *)
 
-val tryAllHyps          : (identifier -> tactic) -> tactic
-val tryAllHypsAndConcl  : (identifier option -> tactic) -> tactic
+val tryAllHyps          : (Id.t -> tactic) -> tactic
+val tryAllHypsAndConcl  : (Id.t option -> tactic) -> tactic
 
-val onAllHyps           : (identifier -> tactic) -> tactic
-val onAllHypsAndConcl   : (identifier option -> tactic) -> tactic
+val onAllHyps           : (Id.t -> tactic) -> tactic
+val onAllHypsAndConcl   : (Id.t option -> tactic) -> tactic
 
-val onClause   : (identifier option -> tactic) -> clause -> tactic
-val onClauseLR : (identifier option -> tactic) -> clause -> tactic
+val onClause   : (Id.t option -> tactic) -> clause -> tactic
+val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
 
 (** {6 Elimination tacticals. } *)
 
@@ -141,8 +141,8 @@ val compute_induction_names :
     intro_pattern_expr located list array
 
 val elimination_sort_of_goal : goal sigma -> sorts_family
-val elimination_sort_of_hyp  : identifier -> goal sigma -> sorts_family
-val elimination_sort_of_clause : identifier option -> goal sigma -> sorts_family
+val elimination_sort_of_hyp  : Id.t -> goal sigma -> sorts_family
+val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family
 
 val general_elim_then_using :
   (inductive -> goal sigma -> constr) -> rec_flag ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 966309395..f6f939ed3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -94,7 +94,7 @@ let string_of_inductive c =
   try match kind_of_term c with
   | Ind ind_sp ->
       let (mib,mip) = Global.lookup_inductive ind_sp in
-      string_of_id mip.mind_typename
+      Id.to_string mip.mind_typename
   | _ -> raise Bound
   with Bound -> error "Bound head variable."
 
@@ -373,8 +373,8 @@ let id_of_name_with_default id = function
   | Anonymous -> id
   | Name id   -> id
 
-let hid = id_of_string "H"
-let xid = id_of_string "X"
+let hid = Id.of_string "H"
+let xid = Id.of_string "X"
 
 let default_id_of_sort = function Prop _ -> hid | Type _ -> xid
 
@@ -389,9 +389,9 @@ let default_id env sigma = function
    possibly a move to do after the introduction *)
 
 type intro_name_flag =
-  | IntroAvoid of identifier list
-  | IntroBasedOn of identifier * identifier list
-  | IntroMustBe of identifier
+  | IntroAvoid of Id.t list
+  | IntroBasedOn of Id.t * Id.t list
+  | IntroMustBe of Id.t
 
 let find_name loc decl gl = function
   | IntroAvoid idl ->
@@ -401,7 +401,7 @@ let find_name loc decl gl = function
   | IntroMustBe id ->
       (* When name is given, we allow to hide a global name *)
       let id' = next_ident_away id (pf_ids_of_hyps gl) in
-      if not (id_eq id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
+      if not (Id.equal id' id) then user_err_loc (loc,"",pr_id id ++ str" is already used.");
       id'
 
 (* Returns the names that would be created by intros, without doing
@@ -468,9 +468,9 @@ let intro_forthcoming_then_gen loc name_flag move_flag dep_flag tac =
   aux []
 
 let rec get_next_hyp_position id = function
-  | [] -> error ("No such hypothesis: " ^ string_of_id id)
+  | [] -> error ("No such hypothesis: " ^ Id.to_string id)
   | (hyp,_,_) :: right ->
-      if id_eq hyp id then
+      if Id.equal hyp id then
 	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast
       else
 	get_next_hyp_position id right
@@ -919,7 +919,7 @@ let descend_in_conjunctions tac exit c gl =
     | Some (_,_,isrec) ->
 	let n = (mis_constr_nargs ind).(0) in
 	let sort = elimination_sort_of_goal gl in
-	let id = fresh_id [] (id_of_string "H") gl in
+	let id = fresh_id [] (Id.of_string "H") gl in
 	let IndType (indf,_) = pf_apply find_rectype gl ccl in
 	let params = snd (dest_ind_family indf) in
 	let cstr = (get_constructors (pf_env gl) indf).(0) in
@@ -1137,7 +1137,7 @@ let clear_wildcards ids =
     with ClearDependencyError (id,err) ->
       (* Intercept standard [thin] error message *)
       Loc.raise loc
-        (error_clear_dependency (pf_env gl) (id_of_string "_") err))
+        (error_clear_dependency (pf_env gl) (Id.of_string "_") err))
     ids
 
 (*   Takes a list of booleans, and introduces all the variables
@@ -1347,17 +1347,17 @@ let rec explicit_intro_names = function
 | [] ->
     []
 
-let wild_id = id_of_string "_tmp"
+let wild_id = Id.of_string "_tmp"
 
 let rec list_mem_assoc_right id = function
   | [] -> false
-  | (x,id')::l -> id_eq id id' || list_mem_assoc_right id l
+  | (x,id')::l -> Id.equal id id' || list_mem_assoc_right id l
 
 let check_thin_clash_then id thin avoid tac =
   if list_mem_assoc_right id thin then
     let newid = next_ident_away (add_suffix id "'") avoid in
     let thin =
-      List.map (on_snd (fun id' -> if id_eq id id' then newid else id')) thin in
+      List.map (on_snd (fun id' -> if Id.equal id id' then newid else id')) thin in
     tclTHEN (rename_hyp [id,newid]) (tac thin)
   else
     tac thin
@@ -1441,7 +1441,7 @@ let ipat_of_name = function
 let allow_replace c gl = function (* A rather arbitrary condition... *)
   | Some (_, IntroIdentifier id) ->
       let c = fst (decompose_app ((strip_lam_assum c))) in
-      isVar c && id_eq (destVar c) id
+      isVar c && Id.equal (destVar c) id
   | _ ->
       false
 
@@ -1631,7 +1631,7 @@ let out_arg = function
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
-    | ((occs,id'),hl)::_ when id_eq id id' ->
+    | ((occs,id'),hl)::_ when Id.equal id id' ->
         Some (occurrences_map (List.map out_arg) occs, hl)
     | _::l -> hyp_occ l in
   match cls.onhyps with
@@ -1684,7 +1684,7 @@ let letin_tac with_eq name c occs gl =
   let id =
     if name = Anonymous then fresh_id [] x gl else
       if not (mem_named_context x (pf_hyps gl)) then x else
-	error ("The variable "^(string_of_id x)^" is already declared") in
+	error ("The variable "^(Id.to_string x)^" is already declared") in
   let (depdecls,marks,ccl)= letin_abstract id c occs gl in
   let t = pf_type_of gl c in
   let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
@@ -1767,7 +1767,7 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs gl =
     let x = id_of_name_using_hdchar (Global.env()) t name in
     if name == Anonymous then fresh_id [] x gl else
       if not (mem_named_context x (pf_hyps gl)) then x else
-	error ("The variable "^(string_of_id x)^" is already declared.") in
+	error ("The variable "^(Id.to_string x)^" is already declared.") in
   let (depdecls,lastlhyp,ccl,c) = letin_abstract id c test occs gl in
   let t = match ty with Some t -> t | None -> pf_apply typ_of gl c in
   let newcl,eq_tac = match with_eq with
@@ -1925,7 +1925,7 @@ let safe_dest_intros_patterns avoid thin dest pat tac gl =
 type elim_arg_kind = RecArg | IndArg | OtherArg
 
 type recarg_position =
-  | AfterFixedPosition of identifier option (* None = top of context *)
+  | AfterFixedPosition of Id.t option (* None = top of context *)
 
 let update_dest (recargdests,tophyp as dests) = function
   | [] -> dests
@@ -2035,15 +2035,15 @@ let find_atomic_param_of_ind nparams indtyp =
   let argl = snd (decompose_app indtyp) in
   let argv = Array.of_list argl in
   let params = List.firstn nparams argl in
-  let indvars = ref Idset.empty in
+  let indvars = ref Id.Set.empty in
   for i = nparams to (Array.length argv)-1 do
     match kind_of_term argv.(i) with
       | Var id
           when not (List.exists (occur_var (Global.env()) id) params) ->
-	  indvars := Idset.add id !indvars
+	  indvars := Id.Set.add id !indvars
       | _ -> ()
   done;
-  Idset.elements !indvars;
+  Id.Set.elements !indvars;
 
 
 (* [cook_sign] builds the lists [indhyps] of hyps that must be
@@ -2109,7 +2109,7 @@ let find_atomic_param_of_ind nparams indtyp =
 
 *)
 
-exception Shunt of identifier move_location
+exception Shunt of Id.t move_location
 
 let cook_sign hyp0_opt indvars env =
   let hyp0,inhyps =
@@ -2126,7 +2126,7 @@ let cook_sign hyp0_opt indvars env =
   let lstatus = ref [] in
   let before = ref true in
   let seek_deps env (hyp,_,_ as decl) rhyp =
-    if id_eq hyp hyp0 then begin
+    if Id.equal hyp hyp0 then begin
       before:=false;
       (* If there was no main induction hypotheses, then hyp is one of
          indvars too, so add it to indhyps. *)
@@ -2154,7 +2154,7 @@ let cook_sign hyp0_opt indvars env =
   let _ = fold_named_context seek_deps env ~init:MoveFirst in
   (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *)
   let compute_lstatus lhyp (hyp,_,_) =
-    if id_eq hyp hyp0 then raise (Shunt lhyp);
+    if Id.equal hyp hyp0 then raise (Shunt lhyp);
     if List.mem hyp !ldeps then begin
       lstatus := (hyp,lhyp)::!lstatus;
       lhyp
@@ -2246,19 +2246,19 @@ let make_base n id =
   else
     (* This extends the name to accept new digits if it already ends with *)
     (* digits *)
-    id_of_string (atompart_of_id (make_ident (string_of_id id) (Some 0)))
+    Id.of_string (atompart_of_id (make_ident (Id.to_string id) (Some 0)))
 
 (* Builds two different names from an optional inductive type and a
    number, also deals with a list of names to avoid. If the inductive
    type is None, then hyprecname is IHi where i is a number. *)
 let make_up_names n ind_opt cname =
   let is_hyp = String.equal (atompart_of_id cname) "H" in
-  let base = string_of_id (make_base n cname) in
+  let base = Id.to_string (make_base n cname) in
   let ind_prefix = "IH" in
   let base_ind =
     if is_hyp then
       match ind_opt with
-	| None -> id_of_string ind_prefix
+	| None -> Id.of_string ind_prefix
 	| Some ind_id -> add_prefix ind_prefix (Nametab.basename_of_global ind_id)
     else add_prefix ind_prefix cname in
   let hyprecname = make_base n base_ind in
@@ -2268,12 +2268,12 @@ let make_up_names n ind_opt cname =
       (* Forbid to use cname, cname0, hyprecname and hyprecname0 *)
       (* in order to get names such as f1, f2, ... *)
       let avoid =
-        (make_ident (string_of_id hyprecname) None) ::
-        (make_ident (string_of_id hyprecname) (Some 0)) :: [] in
+        (make_ident (Id.to_string hyprecname) None) ::
+        (make_ident (Id.to_string hyprecname) (Some 0)) :: [] in
       if not (String.equal (atompart_of_id cname) "H") then
         (make_ident base (Some 0)) :: (make_ident base None) :: avoid
       else avoid in
-  id_of_string base, hyprecname, avoid
+  Id.of_string base, hyprecname, avoid
 
 let error_ind_scheme s =
   let s = if not (String.is_empty s) then s^" " else s in
@@ -2312,7 +2312,7 @@ let lift_list l = List.map (lift 1) l
 let ids_of_constr ?(all=false) vars c =
   let rec aux vars c =
     match kind_of_term c with
-    | Var id -> Idset.add id vars
+    | Var id -> Id.Set.add id vars
     | App (f, args) -> 
 	(match kind_of_term f with
 	| Construct (ind,_)
@@ -2371,17 +2371,17 @@ let make_abstract_generalize gl id concl dep ctx body c eqs args refls =
     mkApp (appeqs, abshypt)
 
 let hyps_of_vars env sign nogen hyps =
-  if Idset.is_empty hyps then [] 
+  if Id.Set.is_empty hyps then [] 
   else
     let (_,lh) =
       Sign.fold_named_context_reverse
         (fun (hs,hl) (x,_,_ as d) ->
-	  if Idset.mem x nogen then (hs,hl)
-	  else if Idset.mem x hs then (hs,x::hl)
+	  if Id.Set.mem x nogen then (hs,hl)
+	  else if Id.Set.mem x hs then (hs,x::hl)
 	  else
 	    let xvars = global_vars_set_of_decl env d in
-	      if not (Idset.equal (Idset.diff xvars hs) Idset.empty) then
-		(Idset.add x hs, x :: hl)
+	      if not (Id.Set.equal (Id.Set.diff xvars hs) Id.Set.empty) then
+		(Id.Set.add x hs, x :: hl)
 	      else (hs, hl))
         ~init:(hyps,[])
         sign 
@@ -2393,11 +2393,11 @@ let linear vars args =
   let seen = ref vars in
     try 
       Array.iter (fun i -> 
-	let rels = ids_of_constr ~all:true Idset.empty i in
+	let rels = ids_of_constr ~all:true Id.Set.empty i in
 	let seen' = 
-	  Idset.fold (fun id acc ->
-	    if Idset.mem id acc then raise Seen
-	    else Idset.add id acc)
+	  Id.Set.fold (fun id acc ->
+	    if Id.Set.mem id acc then raise Seen
+	    else Id.Set.add id acc)
 	    rels !seen
 	in seen := seen')
 	args;
@@ -2415,7 +2415,7 @@ let abstract_args gl generalize_vars dep id defined f args =
   let dep = dep || dependent (mkVar id) concl in
   let avoid = ref [] in
   let get_id name =
-    let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> id_of_string "gen_x") gl in
+    let id = fresh_id !avoid (match name with Name n -> n | Anonymous -> Id.of_string "gen_x") gl in
       avoid := id :: !avoid; id
   in
     (* Build application generalized w.r.t. the argument plus the necessary eqs.
@@ -2436,9 +2436,9 @@ let abstract_args gl generalize_vars dep id defined f args =
     let liftargty = lift lenctx argty in
     let leq = constr_cmp Reduction.CUMUL liftargty ty in
       match kind_of_term arg with
-      | Var id when not (is_defined_variable env id) && leq && not (Idset.mem id nongenvars) ->
+      | Var id when not (is_defined_variable env id) && leq && not (Id.Set.mem id nongenvars) ->
       	  (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls,
-      	  Idset.add id nongenvars, Idset.remove id vars, env)
+      	  Id.Set.add id nongenvars, Id.Set.remove id vars, env)
       | _ ->
 	  let name = get_id name in
 	  let decl = (Name name, None, ty) in
@@ -2456,11 +2456,11 @@ let abstract_args gl generalize_vars dep id defined f args =
 	  let refls = refl :: refls in
 	  let argvars = ids_of_constr vars arg in
 	    (arity, ctx, push_rel decl ctxenv, c', args, eqs, refls, 
-	    nongenvars, Idset.union argvars vars, env)
+	    nongenvars, Id.Set.union argvars vars, env)
   in 
   let f', args' = decompose_indapp f args in
   let dogen, f', args' =
-    let parvars = ids_of_constr ~all:true Idset.empty f' in
+    let parvars = ids_of_constr ~all:true Id.Set.empty f' in
       if not (linear parvars args') then true, f, args
       else
 	match Array.findi (fun i x -> not (isVar x) || is_defined_variable env (destVar x)) args' with
@@ -2471,12 +2471,12 @@ let abstract_args gl generalize_vars dep id defined f args =
   in
     if dogen then
       let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = 
-	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Idset.empty,Idset.empty,env) args'
+	Array.fold_left aux (pf_type_of gl f',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args'
       in
       let args, refls = List.rev args, List.rev refls in
       let vars = 
 	if generalize_vars then
-	  let nogen = Idset.add id nogen in
+	  let nogen = Id.Set.add id nogen in
 	    hyps_of_vars (pf_env gl) (pf_hyps gl) nogen vars
 	else []
       in
@@ -2674,7 +2674,7 @@ let compute_elim_sig ?elimc elimt =
   let params_preds,branches,args_indargs,conclusion =
     decompose_paramspred_branch_args elimt in
 
-  let ccl = exchange_hd_app (mkVar (id_of_string "__QI_DUMMY__")) conclusion in
+  let ccl = exchange_hd_app (mkVar (Id.of_string "__QI_DUMMY__")) conclusion in
   let concl_with_args = it_mkProd_or_LetIn ccl args_indargs in
   let nparams = Int.Set.cardinal (free_rels concl_with_args) in
   let preds,params = cut_list (List.length params_preds - nparams) params_preds in
@@ -2833,11 +2833,11 @@ let find_elim isrec elim hyp0 gl =
     | Some e -> given_elim hyp0 e gl
 
 type scheme_signature =
-    (identifier list * (elim_arg_kind * bool * identifier) list) array
+    (Id.t list * (elim_arg_kind * bool * Id.t) list) array
 
 type eliminator_source =
   | ElimUsing of (eliminator * types) * scheme_signature
-  | ElimOver of bool * identifier
+  | ElimOver of bool * Id.t
 
 let find_induction_type isrec elim hyp0 gl =
   let scheme,elim =
@@ -3299,7 +3299,7 @@ let andE id gl =
     (tclTHEN (simplest_elim (mkVar id)) (tclDO 2 intro)) gl
   else
     errorlabstrm "andE"
-      (str("Tactic andE expects "^(string_of_id id)^" is a conjunction."))
+      (str("Tactic andE expects "^(Id.to_string id)^" is a conjunction."))
 
 let dAnd cls =
   onClause
@@ -3314,7 +3314,7 @@ let orE id gl =
     (tclTHEN (simplest_elim (mkVar id)) intro) gl
   else
     errorlabstrm "orE"
-      (str("Tactic orE expects "^(string_of_id id)^" is a disjunction."))
+      (str("Tactic orE expects "^(Id.to_string id)^" is a disjunction."))
 
 let dorE b cls =
   onClause
@@ -3332,7 +3332,7 @@ let impE id gl =
       (apply_term (mkVar id) [mkMeta (new_meta())]) gl
   else
     errorlabstrm "impE"
-      (str("Tactic impE expects "^(string_of_id id)^
+      (str("Tactic impE expects "^(Id.to_string id)^
 	      " is a an implication."))
 
 let dImp cls =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f33ef1bc5..041edd250 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -38,44 +38,44 @@ open Locus
 val string_of_inductive : constr -> string
 val head_constr       : constr -> constr * constr list
 val head_constr_bound : constr -> constr * constr list
-val is_quantified_hypothesis : identifier -> goal sigma -> bool
+val is_quantified_hypothesis : Id.t -> goal sigma -> bool
 
 exception Bound
 
 (** {6 Primitive tactics. } *)
 
-val introduction    : identifier -> tactic
+val introduction    : Id.t -> tactic
 val refine          : constr -> tactic
 val convert_concl   : constr -> cast_kind -> tactic
 val convert_hyp     : named_declaration -> tactic
-val thin            : identifier list -> tactic
+val thin            : Id.t list -> tactic
 val mutual_fix      :
-  identifier -> int -> (identifier * int * constr) list -> int -> tactic
-val fix             : identifier option -> int -> tactic
-val mutual_cofix    : identifier -> (identifier * constr) list -> int -> tactic
-val cofix           : identifier option -> tactic
+  Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
+val fix             : Id.t option -> int -> tactic
+val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
+val cofix           : Id.t option -> tactic
 
 (** {6 Introduction tactics. } *)
 
-val fresh_id_in_env : identifier list -> identifier -> env -> identifier
-val fresh_id : identifier list -> identifier -> goal sigma -> identifier
-val find_intro_names : rel_context -> goal sigma -> identifier list
+val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t
+val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t
+val find_intro_names : rel_context -> goal sigma -> Id.t list
 
 val intro                : tactic
 val introf               : tactic
-val intro_move        : identifier option -> identifier move_location -> tactic
+val intro_move        : Id.t option -> Id.t move_location -> tactic
 
-  (** [intro_avoiding idl] acts as intro but prevents the new identifier
+  (** [intro_avoiding idl] acts as intro but prevents the new Id.t
      to belong to [idl] *)
-val intro_avoiding       : identifier list -> tactic
+val intro_avoiding       : Id.t list -> tactic
 
-val intro_replacing      : identifier -> tactic
-val intro_using          : identifier -> tactic
-val intro_mustbe_force   : identifier -> tactic
-val intro_then           : (identifier -> tactic) -> tactic
-val intros_using         : identifier list -> tactic
-val intro_erasing        : identifier -> tactic
-val intros_replacing     : identifier list -> tactic
+val intro_replacing      : Id.t -> tactic
+val intro_using          : Id.t -> tactic
+val intro_mustbe_force   : Id.t -> tactic
+val intro_then           : (Id.t -> tactic) -> tactic
+val intros_using         : Id.t list -> tactic
+val intro_erasing        : Id.t -> tactic
+val intros_replacing     : Id.t list -> tactic
 
 val intros               : tactic
 
@@ -96,7 +96,7 @@ val intros_clearing      : bool list -> tactic
    hypothesis is already in context and directly apply [tac] *)
 
 val try_intros_until :
-  (identifier -> tactic) -> quantified_hypothesis -> tactic
+  (Id.t -> tactic) -> quantified_hypothesis -> tactic
 
 (** Apply a tactic on a quantified hypothesis, an hypothesis in context
    or a term with bindings *)
@@ -107,10 +107,10 @@ val onInductionArg :
 
 (** {6 Introduction tactics with eliminations. } *)
 
-val intro_pattern  : identifier move_location -> intro_pattern_expr -> tactic
+val intro_pattern  : Id.t move_location -> intro_pattern_expr -> tactic
 val intro_patterns : intro_pattern_expr located list -> tactic
 val intros_pattern :
-  identifier move_location -> intro_pattern_expr located list -> tactic
+  Id.t move_location -> intro_pattern_expr located list -> tactic
 
 (** {6 Exact tactics. } *)
 
@@ -159,16 +159,16 @@ val unfold_constr     : global_reference -> tactic
 
 (** {6 Modification of the local context. } *)
 
-val clear         : identifier list -> tactic
-val clear_body    : identifier list -> tactic
-val keep          : identifier list -> tactic
+val clear         : Id.t list -> tactic
+val clear_body    : Id.t list -> tactic
+val keep          : Id.t list -> tactic
 
 val specialize    : int option -> constr with_bindings -> tactic
 
-val move_hyp      : bool -> identifier -> identifier move_location -> tactic
-val rename_hyp    : (identifier * identifier) list -> tactic
+val move_hyp      : bool -> Id.t -> Id.t move_location -> tactic
+val rename_hyp    : (Id.t * Id.t) list -> tactic
 
-val revert        : identifier list -> tactic
+val revert        : Id.t list -> tactic
 
 (** {6 Resolution tactics. } *)
 
@@ -188,11 +188,11 @@ val eapply_with_bindings  : constr with_bindings -> tactic
 val cut_and_apply         : constr -> tactic
 
 val apply_in :
-  advanced_flag -> evars_flag -> identifier -> 
+  advanced_flag -> evars_flag -> Id.t -> 
     constr with_bindings located list ->
     intro_pattern_expr located option -> tactic
 
-val simple_apply_in : identifier -> constr -> tactic
+val simple_apply_in : Id.t -> constr -> tactic
 
 (** {6 Elimination tactics. } *)
 
@@ -257,14 +257,14 @@ val elimination_clause_scheme : evars_flag -> ?flags:unify_flags ->
   int -> clausenv -> clausenv -> tactic
 
 val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> 
-  identifier -> int -> clausenv -> clausenv -> tactic
+  Id.t -> int -> clausenv -> clausenv -> tactic
 
 val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) ->
   'a -> eliminator -> tactic
 
 val general_elim  : evars_flag ->
   constr with_bindings -> eliminator -> tactic
-val general_elim_in : evars_flag -> identifier ->
+val general_elim_in : evars_flag -> Id.t ->
   constr with_bindings -> eliminator -> tactic
 
 val default_elim  : evars_flag -> constr with_bindings -> tactic
@@ -308,9 +308,9 @@ val elim_type         : constr  -> tactic
 
 (** {6 Some eliminations which are frequently used. } *)
 
-val impE : identifier -> tactic
-val andE : identifier -> tactic
-val orE  : identifier -> tactic
+val impE : Id.t -> tactic
+val andE : Id.t -> tactic
+val orE  : Id.t -> tactic
 val dImp : clause -> tactic
 val dAnd : clause -> tactic
 val dorE : bool -> clause ->tactic
@@ -345,8 +345,8 @@ val intros_reflexivity          : tactic
 val register_setoid_symmetry : tactic -> unit
 val symmetry_red                : bool -> tactic
 val symmetry                    : tactic
-val register_setoid_symmetry_in : (identifier -> tactic) -> unit
-val symmetry_in                 : identifier -> tactic
+val register_setoid_symmetry_in : (Id.t -> tactic) -> unit
+val symmetry_in                 : Id.t -> tactic
 val intros_symmetry             : clause -> tactic
 
 val register_setoid_transitivity : (constr option -> tactic) -> unit
@@ -357,8 +357,8 @@ val intros_transitivity         : constr option -> tactic
 
 val cut                         : constr -> tactic
 val cut_intro                   : constr -> tactic
-val assert_replacing            : identifier -> types -> tactic -> tactic
-val cut_replacing               : identifier -> types -> tactic -> tactic
+val assert_replacing            : Id.t -> types -> tactic -> tactic
+val cut_replacing               : Id.t -> types -> tactic -> tactic
 val cut_in_parallel             : constr list -> tactic
 
 val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic
@@ -378,15 +378,15 @@ val generalize_dep  : ?with_let:bool (** Don't lose let bindings *) -> constr  -
 val unify           : ?state:Names.transparent_state -> constr -> constr -> tactic
 val resolve_classes : tactic
 
-val tclABSTRACT : identifier option -> tactic -> tactic
+val tclABSTRACT : Id.t option -> tactic -> tactic
 
 val admit_as_an_axiom : tactic
 
-val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> identifier -> tactic
-val specialize_eqs : identifier -> tactic
+val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> tactic
+val specialize_eqs : Id.t -> tactic
 
 val register_general_multi_rewrite :
   (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit
 
 val register_subst_one :
-  (bool -> identifier -> identifier * constr * bool -> tactic) -> unit
+  (bool -> Id.t -> Id.t * constr * bool -> tactic) -> unit
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 5b41e0b3b..fbae96651 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -20,7 +20,7 @@ open Errors
 open Util
 
 let assoc_var s ist =
-  match List.assoc (Names.id_of_string s) ist.lfun with
+  match List.assoc (Names.Id.of_string s) ist.lfun with
     | VConstr ([],c) -> c
     | _ -> failwith "tauto: anomaly"
 
@@ -297,8 +297,8 @@ let tauto_intuitionistic flags g =
       errorlabstrm "tauto" (str "tauto failed.")
 
 let coq_nnpp_path =
-  let dir = List.map id_of_string ["Classical_Prop";"Logic";"Coq"] in
-  Libnames.make_path (make_dirpath dir) (id_of_string "NNPP")
+  let dir = List.map Id.of_string ["Classical_Prop";"Logic";"Coq"] in
+  Libnames.make_path (make_dirpath dir) (Id.of_string "NNPP")
 
 let tauto_classical flags nnpp g =
   try tclTHEN (apply nnpp) (tauto_intuitionistic flags) g
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 268c6a2e8..becd19a66 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -85,9 +85,9 @@ let constr_pat_discr_st (idpred,cpred) t =
   match decomp_pat t with
   | PRef ((IndRef _) as ref), args
   | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args)
-  | PRef ((VarRef v) as ref), args when not (Idpred.mem v idpred) ->
+  | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) ->
       Some(GRLabel ref,args)
-  | PVar v, args when not (Idpred.mem v idpred) ->
+  | PVar v, args when not (Id.Pred.mem v idpred) ->
       Some(GRLabel (VarRef v),args)
   | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) ->
       Some (GRLabel ref, args)
@@ -113,7 +113,7 @@ let constr_val_discr_st (idpred,cpred) t =
     | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l)
     | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l)
     | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l)
-    | Var id when not (Idpred.mem id idpred) -> Label(GRLabel (VarRef id),l)
+    | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l)
     | Prod (n, d, c) -> Label(ProdLabel, [d; c])
     | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l)
     | Sort _ -> Label (SortLabel, [])