Modulification of identifier

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

36 files changed, 209 insertions, 209 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c02dbba23..a92e37480 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -73,7 +73,7 @@ let rec list_try_compile f = function
 	    list_try_compile f t
 
 let force_name =
-  let nx = Name (id_of_string "x") in function Anonymous -> nx | na -> na
+  let nx = Name (Id.of_string "x") in function Anonymous -> nx | na -> na
 
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
@@ -107,8 +107,8 @@ let rec relocate_index n1 n2 k t = match kind_of_term t with
 
 type 'a rhs =
     { rhs_env    : env;
-      rhs_vars   : identifier list;
-      avoid_ids  : identifier list;
+      rhs_vars   : Id.t list;
+      avoid_ids  : Id.t list;
       it         : 'a option}
 
 type 'a equation =
@@ -1807,7 +1807,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
       let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in
       let sigma = !evdref in
       (* let sigma = Option.cata (fun tycon -> *)
-      (*     let na = Name (id_of_string "x") in *)
+      (*     let na = Name (Id.of_string "x") in *)
       (*     let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in *)
       (*     let predinst = extract_predicate predcclj.uj_val tms in *)
       (*     Coercion.inh_conv_coerce_to loc env !evdref predinst tycon) *)
@@ -1830,11 +1830,11 @@ let ($) f x = f x
 let string_of_name name =
   match name with
     | Anonymous -> "anonymous"
-    | Name n -> string_of_id n
+    | Name n -> Id.to_string n
 
 let make_prime_id name =
   let str = string_of_name name in
-    id_of_string str, id_of_string (str ^ "'")
+    Id.of_string str, Id.of_string (str ^ "'")
 
 let prime avoid name =
   let previd, id = make_prime_id name in
@@ -1846,7 +1846,7 @@ let make_prime avoid prevname =
     previd, id
 
 let eq_id avoid id =
-  let hid = id_of_string ("Heq_" ^ string_of_id id) in
+  let hid = Id.of_string ("Heq_" ^ Id.to_string id) in
   let hid' = next_ident_away hid avoid in
     hid'
 
@@ -1865,7 +1865,7 @@ let constr_of_pat env isevars arsign pat avoid =
 	let name, avoid = match name with
 	    Name n -> name, avoid
 	  | Anonymous ->
-	      let previd, id = prime avoid (Name (id_of_string "wildcard")) in
+	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
 		Name id, id :: avoid
 	in
 	  (PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, 
@@ -1931,7 +1931,7 @@ let constr_of_pat env isevars arsign pat avoid =
 
 (* shadows functional version *)
 let eq_id avoid id =
-  let hid = id_of_string ("Heq_" ^ string_of_id id) in
+  let hid = Id.of_string ("Heq_" ^ Id.to_string id) in
   let hid' = next_ident_away hid !avoid in
     avoid := hid' :: !avoid;
     hid'
@@ -1960,7 +1960,7 @@ let vars_of_ctx ctx =
 	    match na with
 		Anonymous -> raise (Invalid_argument "vars_of_ctx")
 	      | Name n -> n, GVar (Loc.ghost, n) :: vars)
-      ctx (id_of_string "vars_of_ctx_error", [])
+      ctx (Id.of_string "vars_of_ctx_error", [])
   in List.rev y
 
 let rec is_included x y =
@@ -2075,7 +2075,7 @@ let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
 	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
 	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
 	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
-	 let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
+	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
 	 let branch =
 	   let bref = GVar (Loc.ghost, branch_name) in
@@ -2123,7 +2123,7 @@ let abstract_tomatch env tomatchs tycon =
 	   | _ ->
 	       let tycon = Option.map
 		 (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in
-	       let name = next_ident_away (id_of_string "filtered_var") names in
+	       let name = next_ident_away (Id.of_string "filtered_var") names in
 		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
 	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
 	       name :: names, tycon)
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 9d0a6c9c3..d1ca69dcd 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -59,16 +59,16 @@ val constr_of_pat :
            Evd.evar_map ref ->
            Term.rel_declaration list ->
            Glob_term.cases_pattern ->
-           Names.identifier list ->
+           Names.Id.t list ->
            Glob_term.cases_pattern *
            (Term.rel_declaration list * Term.constr *
             (Term.types * Term.constr list) * Glob_term.cases_pattern) *
-           Names.identifier list
+           Names.Id.t list
 
 type 'a rhs =
     { rhs_env    : env;
-      rhs_vars   : identifier list;
-      avoid_ids  : identifier list;
+      rhs_vars   : Id.t list;
+      avoid_ids  : Id.t list;
       it         : 'a option}
 
 type 'a equation =
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index d8cfde590..ebdfcdbe6 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -56,7 +56,7 @@ let coe_info_typ_equal c1 c2 =
 let cl_typ_eq t1 t2 = match t1, t2 with
 | CL_SORT, CL_SORT -> true
 | CL_FUN, CL_FUN -> true
-| CL_SECVAR v1, CL_SECVAR v2 -> id_eq v1 v2
+| CL_SECVAR v1, CL_SECVAR v2 -> Id.equal v1 v2
 | CL_CONST c1, CL_CONST c2 -> eq_constant c1 c2
 | CL_IND i1, CL_IND i2 -> eq_ind i1 i2
 | _ -> false
@@ -201,11 +201,11 @@ let string_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
   | CL_CONST sp ->
-      string_of_qualid (shortest_qualid_of_global Idset.empty (ConstRef sp))
+      string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
   | CL_IND sp ->
-      string_of_qualid (shortest_qualid_of_global Idset.empty (IndRef sp))
+      string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
   | CL_SECVAR sp ->
-      string_of_qualid (shortest_qualid_of_global Idset.empty (VarRef sp))
+      string_of_qualid (shortest_qualid_of_global Id.Set.empty (VarRef sp))
 
 let pr_class x = str (string_of_class x)
 
@@ -444,7 +444,7 @@ let coercion_of_reference r =
   let ref = Nametab.global r in
   if not (coercion_exists ref) then
     errorlabstrm "try_add_coercion"
-      (Nametab.pr_global_env Idset.empty ref ++ str" is not a coercion.");
+      (Nametab.pr_global_env Id.Set.empty ref ++ str" is not a coercion.");
   ref
 
 module CoercionPrinting =
@@ -452,7 +452,7 @@ module CoercionPrinting =
     type t = coe_typ
     let encode = coercion_of_reference
     let subst = subst_coe_typ
-    let printer x = pr_global_env Idset.empty x
+    let printer x = pr_global_env Id.Set.empty x
     let key = ["Printing";"Coercion"]
     let title = "Explicitly printed coercions: "
     let member_message x b =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 888e4e388..b398a5693 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -70,7 +70,7 @@ let app_opt env evars f t =
   whd_betaiota !evars (app_opt f t)
 
 let pair_of_array a = (a.(0), a.(1))
-let make_name s = Name (id_of_string s)
+let make_name s = Name (Id.of_string s)
 
 let disc_subset x =
   match kind_of_term x with
@@ -174,7 +174,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
 	   | Type x, Type y when Univ.Universe.equal x y -> None (* false *)
 	   | _ -> subco ())
       | Prod (name, a, b), Prod (name', a', b') ->
-	  let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
+	  let name' = Name (Namegen.next_ident_away (Id.of_string "x") (Termops.ids_of_context env)) in
 	  let env' = push_rel (name', None, a') env in
 	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 	    (* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
@@ -435,7 +435,7 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
           (* Note: we retype the term because sort-polymorphism may have *)
           (* weaken its type *)
 	  let name = match name with
-	    | Anonymous -> Name (id_of_string "x")
+	    | Anonymous -> Name (Id.of_string "x")
 	    | _ -> name in
 	  let env1 = push_rel (name,None,u1) env in
 	  let (evd', v1) =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index a96deca06..af8cc43c1 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -74,7 +74,7 @@ module PrintingInductiveMake =
       let kn' = subst_ind subst kn in
 	if kn' == kn then obj else
 	  kn', ints
-    let printer ind = pr_global_env Idset.empty (IndRef ind)
+    let printer ind = pr_global_env Id.Set.empty (IndRef ind)
     let key = ["Printing";Test.field]
     let title = Test.title
     let member_message x = Test.member_message (printer x)
@@ -175,11 +175,11 @@ let lookup_name_as_displayed env t s =
   let rec lookup avoid n c = match kind_of_term c with
     | Prod (name,_,c') ->
 	(match compute_displayed_name_in RenamingForGoal avoid name c' with
-           | (Name id,avoid') -> if id_eq id s then Some n else lookup avoid' (n+1) c'
+           | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | LetIn (name,_,_,c') ->
 	(match compute_displayed_name_in RenamingForGoal avoid name c' with
-           | (Name id,avoid') -> if id_eq id s then Some n else lookup avoid' (n+1) c'
+           | (Name id,avoid') -> if Id.equal id s then Some n else lookup avoid' (n+1) c'
 	   | (Anonymous,avoid') -> lookup avoid' (n+1) (pop c'))
     | Cast (c,_,_) -> lookup avoid n c
     | _ -> None
@@ -231,7 +231,7 @@ let rec decomp_branch n nal b (avoid,env as e) c =
 	| Lambda (na,_,c) -> na,c,compute_displayed_let_name_in
 	| LetIn (na,_,_,c) -> na,c,compute_displayed_name_in
 	| _ ->
-	    Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])),
+	    Name (Id.of_string "x"),(applist (lift 1 c, [mkRel 1])),
 	    compute_displayed_name_in in
     let na',avoid' = f flag avoid na c in
     decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c
@@ -293,7 +293,7 @@ let it_destRLambda_or_LetIn_names n c =
       | _ ->
           (* eta-expansion *)
 	  let next l =
-	    let x = next_ident_away (id_of_string "x") l in
+	    let x = next_ident_away (Id.of_string "x") l in
 	    (* Not efficient but unusual and no function to get free glob_vars *)
 (* 	    if occur_glob_constr x c then next (x::l) else x in *)
 	    x
@@ -386,7 +386,7 @@ let rec detype (isgoal:bool) avoid env t =
 	 | Anonymous -> !detype_anonymous dl n
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
-	 in GVar (dl, id_of_string s))
+	 in GVar (dl, Id.of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
 	GEvar (dl, n, None)
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 6c1e1265f..1e31e04d4 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -29,23 +29,23 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr
    [isgoal] tells if naming must avoid global-level synonyms as intro does 
    [ctx] gives the names of the free variables *)
 
-val detype : bool -> identifier list -> names_context -> constr -> glob_constr
+val detype : bool -> Id.t list -> names_context -> constr -> glob_constr
 
 val detype_case :
   bool -> ('a -> glob_constr) ->
   (constructor array -> int array -> 'a array ->
-    (Loc.t * identifier list * cases_pattern list * glob_constr) list) ->
+    (Loc.t * Id.t list * cases_pattern list * glob_constr) list) ->
   ('a -> int -> bool) ->
-  identifier list -> inductive * case_style * int array * int ->
+  Id.t list -> inductive * case_style * int array * int ->
     'a option -> 'a -> 'a array -> glob_constr
 
 val detype_sort : sorts -> glob_sort
 
-val detype_rel_context : constr option -> identifier list -> names_context ->
+val detype_rel_context : constr option -> Id.t list -> names_context ->
   rel_context -> glob_decl list
 
 (** look for the index of a named var or a nondep var as it is renamed *)
-val lookup_name_as_displayed  : env -> constr -> identifier -> int option
+val lookup_name_as_displayed  : env -> constr -> Id.t -> int option
 val lookup_index_as_renamed : env -> constr -> int -> int option
 
 val set_detype_anonymous : (Loc.t -> int -> glob_constr) -> unit
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3cf0c50ba..d9f857c4e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -595,8 +595,8 @@ let filter_possible_projections c ty ctxt args =
     (* interested in finding a term u convertible to c such that a occurs *)
     (* in u *)
     isRel a && Int.Set.mem (destRel a) fv1 ||
-    isVar a && Idset.mem (destVar a) fv2 ||
-    Idset.mem id tyvars)
+    isVar a && Id.Set.mem (destVar a) fv2 ||
+    Id.Set.mem id tyvars)
     ctxt args
 
 let solve_evars = ref (fun _ -> failwith "solve_evars not installed")
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b82f18da7..b6e8f9d13 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -440,12 +440,12 @@ let compute_var_aliases sign =
         (match kind_of_term t with
         | Var id' ->
             let aliases_of_id =
-              try Idmap.find id' aliases with Not_found -> [] in
-            Idmap.add id (aliases_of_id@[t]) aliases
+              try Id.Map.find id' aliases with Not_found -> [] in
+            Id.Map.add id (aliases_of_id@[t]) aliases
 	| _ ->
-            Idmap.add id [t] aliases)
+            Id.Map.add id [t] aliases)
     | None -> aliases)
-    sign Idmap.empty
+    sign Id.Map.empty
 
 let compute_rel_aliases var_aliases rels =
   snd (List.fold_right (fun (_,b,t) (n,aliases) ->
@@ -455,7 +455,7 @@ let compute_rel_aliases var_aliases rels =
          (match kind_of_term t with
          | Var id' ->
              let aliases_of_n =
-               try Idmap.find id' var_aliases with Not_found -> [] in
+               try Id.Map.find id' var_aliases with Not_found -> [] in
              Int.Map.add n (aliases_of_n@[t]) aliases
          | Rel p ->
              let aliases_of_n =
@@ -480,7 +480,7 @@ let lift_aliases n (var_aliases,rel_aliases as aliases) =
 
 let get_alias_chain_of aliases x = match kind_of_term x with
   | Rel n -> (try Int.Map.find n (snd aliases) with Not_found -> [])
-  | Var id -> (try Idmap.find id (fst aliases) with Not_found -> [])
+  | Var id -> (try Id.Map.find id (fst aliases) with Not_found -> [])
   | _ -> []
 
 let normalize_alias_opt aliases x =
@@ -508,7 +508,7 @@ let extend_alias (_,b,_) (var_aliases,rel_aliases) =
         (match kind_of_term t with
         | Var id' ->
             let aliases_of_binder =
-              try Idmap.find id' var_aliases with Not_found -> [] in
+              try Id.Map.find id' var_aliases with Not_found -> [] in
 	    Int.Map.add 1 (aliases_of_binder@[t]) rel_aliases
         | Rel p ->
             let aliases_of_binder =
@@ -545,15 +545,15 @@ let rec expand_vars_in_term_using aliases t = match kind_of_term t with
 let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
 
 let free_vars_and_rels_up_alias_expansion aliases c =
-  let acc1 = ref Int.Set.empty and acc2 = ref Idset.empty in
-  let cache_rel = ref Int.Set.empty and cache_var = ref Idset.empty in
+  let acc1 = ref Int.Set.empty and acc2 = ref Id.Set.empty in
+  let cache_rel = ref Int.Set.empty and cache_var = ref Id.Set.empty in
   let is_in_cache depth = function
     | Rel n -> Int.Set.mem (n-depth) !cache_rel
-    | Var s -> Idset.mem s !cache_var
+    | Var s -> Id.Set.mem s !cache_var
     | _ -> false in
   let put_in_cache depth = function
     | Rel n -> cache_rel := Int.Set.add (n-depth) !cache_rel
-    | Var s -> cache_var := Idset.add s !cache_var
+    | Var s -> cache_var := Id.Set.add s !cache_var
     | _ -> () in
   let rec frec (aliases,depth) c =
     match kind_of_term c with
@@ -562,11 +562,11 @@ let free_vars_and_rels_up_alias_expansion aliases c =
       put_in_cache depth ck;
       let c = expansion_of_var aliases c in
         match kind_of_term c with
-        | Var id -> acc2 := Idset.add id !acc2
+        | Var id -> acc2 := Id.Set.add id !acc2
         | Rel n -> if n >= depth+1 then acc1 := Int.Set.add (n-depth) !acc1
         | _ -> frec (aliases,depth) c end
     | Const _ | Ind _ | Construct _ ->
-        acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2
+        acc2 := List.fold_right Id.Set.add (vars_of_global (Global.env()) c) !acc2
     | _ ->
         iter_constr_with_full_binders
           (fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
@@ -580,10 +580,10 @@ let free_vars_and_rels_up_alias_expansion aliases c =
 (************************************)
 
 type clear_dependency_error =
-| OccurHypInSimpleClause of identifier option
+| OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of existential
 
-exception ClearDependencyError of identifier * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error
 
 open Store.Field
 
@@ -624,7 +624,7 @@ let rec check_and_clear_in_constr evdref err ids c =
 		  (* Check if some id to clear occurs in the instance
 		     a of rid in ev and remember the dependency *)
 		  match
-		    List.filter (fun id -> List.mem id ids) (Idset.elements (collect_vars a))
+		    List.filter (fun id -> List.mem id ids) (Id.Set.elements (collect_vars a))
 		  with
 		  | id :: _ -> (hy,ar,(rid,id)::ri)
 		  | _ ->
@@ -680,7 +680,7 @@ let clear_hyps_in_evi evdref hyps concl ids =
       match !vk with
 	| VKnone -> vk
 	| VKvalue (v,d) ->
-	    if (List.for_all (fun e -> not (Idset.mem e d)) ids) then
+	    if (List.for_all (fun e -> not (Id.Set.mem e d)) ids) then
 	      (* v does depend on any of ids, it's ok *)
 	      vk
 	    else
@@ -728,7 +728,7 @@ let get_actual_deps aliases l t =
     let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
     List.filter (fun c ->
       match kind_of_term c with
-      | Var id -> Idset.mem id fv_ids
+      | Var id -> Id.Set.mem id fv_ids
       | Rel n -> Int.Set.mem n fv_rels
       | _ -> assert false) l
 
@@ -838,23 +838,23 @@ let make_projectable_subst aliases sigma evi args =
 		  let l = try Constrmap.find cstr cstrs with Not_found -> [] in
 		  Constrmap.add cstr ((args,id)::l) cstrs
 	      | _ -> cstrs in
-	    (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
+	    (rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
 	| Some c, a::rest ->
 	    let a = whd_evar sigma a in
 	    (match kind_of_term c with
 	    | Var id' ->
 		let idc = normalize_alias_var evar_aliases id' in
-		let sub = try Idmap.find idc all with Not_found -> [] in
+		let sub = try Id.Map.find idc all with Not_found -> [] in
 		if List.exists (fun (c,_,_) -> eq_constr a c) sub then
 		  (rest,all,cstrs)
 		else
 		  (rest,
-		   Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
+		   Id.Map.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
 		   cstrs)
 	    | _ ->
-		(rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
+		(rest,Id.Map.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
 	| _ -> anomaly "Instance does not match its signature")
-      sign (Array.rev_to_list args,Idmap.empty,Constrmap.empty) in
+      sign (Array.rev_to_list args,Id.Map.empty,Constrmap.empty) in
   (full_subst,cstr_subst)
 
 let make_pure_subst evi args =
@@ -993,10 +993,10 @@ let find_projectable_constructor env evd cstr k args cstr_subst =
 
 type evar_projection =
 | ProjectVar
-| ProjectEvar of existential * evar_info * identifier * evar_projection
+| ProjectEvar of existential * evar_info * Id.t * evar_projection
 
 exception NotUnique
-exception NotUniqueInType of (identifier * evar_projection) list
+exception NotUniqueInType of (Id.t * evar_projection) list
 
 let rec assoc_up_to_alias sigma aliases y yc = function
   | [] -> raise Not_found
@@ -1039,7 +1039,7 @@ let rec find_projectable_vars with_evars aliases sigma y subst =
 	| _ -> anomaly "More than one non var in aliases class of evar instance"
       else
 	subst' in
-  Idmap.fold is_projectable subst []
+  Id.Map.fold is_projectable subst []
 
 (* [filter_solution] checks if one and only one possible projection exists
  * among a set of solutions to a projection problem *)
@@ -1199,13 +1199,13 @@ let filter_candidates evd evk filter candidates =
   | Some l, Some filter ->
       let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in
       Some (List.filter (fun a ->
-        List.subset (Idset.elements (collect_vars a)) ids) l)
+        List.subset (Id.Set.elements (collect_vars a)) ids) l)
 
 let closure_of_filter evd evk filter =
   let evi = Evd.find_undefined evd evk in
   let vars = collect_vars (evar_concl evi) in
   let ids = List.map pi1 (evar_context evi) in
-  let test id b = b || Idset.mem id vars in
+  let test id b = b || Id.Set.mem id vars in
   let newfilter = List.map2 test ids filter in
   if eq_filter newfilter (evar_filter evi) then None else Some newfilter
 
@@ -1372,7 +1372,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
   | Ind _ -> Array.for_all (is_constrainable_in k g) args
   | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
   | Evar (ev',_) -> not (Int.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
-  | Var id -> Idset.mem id fv_ids
+  | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | Sort _ -> true
   | _ -> (* We don't try to be more clever *) true
@@ -1380,7 +1380,7 @@ let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
 let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
   let t = expansion_of_var aliases t in
   match kind_of_term t with
-  | Var id -> Idset.mem id fv_ids
+  | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
   | _ -> is_constrainable_in k (ev,fvs) t
 
@@ -1536,7 +1536,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
  *)
 
 exception NotInvertibleUsingOurAlgorithm of constr
-exception NotEnoughInformationToProgress of (identifier * evar_projection) list
+exception NotEnoughInformationToProgress of (Id.t * evar_projection) list
 exception OccurCheckIn of evar_map * constr
 
 let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
@@ -1954,7 +1954,7 @@ let empty_valcon = None
 (* Builds a value constraint *)
 let mk_valcon c = Some c
 
-let idx = id_of_string "x"
+let idx = Id.of_string "x"
 
 (* Refining an evar to a product *)
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index fb53654de..b056cd260 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -51,7 +51,7 @@ val new_type_evar :
 val new_evar_instance :
  named_context_val -> evar_map -> types -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> constr list -> evar_map * constr
 
-val make_pure_subst : evar_info -> constr array -> (identifier * constr) list
+val make_pure_subst : evar_info -> constr array -> (Id.t * constr) list
 
 (** {6 Instantiate evars} *)
 
@@ -201,17 +201,17 @@ val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
 type clear_dependency_error =
-| OccurHypInSimpleClause of identifier option
+| OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of existential
 
-exception ClearDependencyError of identifier * clear_dependency_error
+exception ClearDependencyError of Id.t * clear_dependency_error
 
 (* spiwack: marks an evar that has been "defined" by clear.
     used by [Goal] and (indirectly) [Proofview] to handle the clear tactic gracefully*)
 val cleared : bool Store.Field.t
 
 val clear_hyps_in_evi : evar_map ref -> named_context_val -> types ->
-  identifier list -> named_context_val * types
+  Id.t list -> named_context_val * types
 
 val push_rel_context_to_named_context : Environ.env -> types ->
   named_context_val * types * constr list * constr list
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index a4e314873..a73dbdcdc 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -217,7 +217,7 @@ val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_
 val meta_type      : evar_map -> metavariable -> types
 val meta_ftype     : evar_map -> metavariable -> types freelisted
 val meta_name      : evar_map -> metavariable -> name
-val meta_with_name : evar_map -> identifier -> metavariable
+val meta_with_name : evar_map -> Id.t -> metavariable
 val meta_declare   :
   metavariable -> types -> ?name:name -> evar_map -> evar_map
 val meta_assign    : metavariable -> constr * instance_status -> evar_map -> evar_map
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 8bd8dc217..65c21f1be 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -117,11 +117,11 @@ let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
 let same_id na id = match na with
 | Anonymous -> false
-| Name id' -> id_eq id id'
+| Name id' -> Id.equal id id'
 
 let occur_glob_constr id =
   let rec occur = function
-    | GVar (loc,id') -> id_eq id id'
+    | GVar (loc,id') -> Id.equal id id'
     | GApp (loc,f,args) -> (occur f) or (List.exists occur args)
     | GLambda (loc,na,bk,ty,c) ->
       (occur ty) || (not (same_id na id) && (occur c))
@@ -141,13 +141,13 @@ let occur_glob_constr id =
     | GRec (loc,fk,idl,bl,tyl,bv) ->
         not (Array.for_all4 (fun fid bl ty bd ->
           let rec occur_fix = function
-              [] -> not (occur ty) && (id_eq fid id || not(occur bd))
+              [] -> not (occur ty) && (Id.equal fid id || not(occur bd))
             | (na,k,bbd,bty)::bl ->
                 not (occur bty) &&
                 (match bbd with
                     Some bd -> not (occur bd)
                   | _ -> true) &&
-                (match na with Name id' -> id_eq id id' | _ -> not (occur_fix bl)) in
+                (match na with Name id' -> Id.equal id id' | _ -> not (occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
     | GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false)
@@ -165,11 +165,11 @@ let occur_glob_constr id =
 let add_name_to_ids set na =
   match na with
     | Anonymous -> set
-    | Name id -> Idset.add id set
+    | Name id -> Id.Set.add id set
 
 let free_glob_vars  =
   let rec vars bounded vs = function
-    | GVar (loc,id') -> if Idset.mem id' bounded then vs else Idset.add id' vs
+    | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
     | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
     | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
 	let vs' = vars bounded vs ty in
@@ -190,7 +190,7 @@ let free_glob_vars  =
 	let vs3 = vars bounded vs2 b1 in
 	vars bounded vs3 b2
     | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bounded' = Array.fold_right Idset.add idl bounded in
+	let bounded' = Array.fold_right Id.Set.add idl bounded in
 	let vars_fix i vs fid =
 	  let vs1,bounded1 =
 	    List.fold_left
@@ -212,7 +212,7 @@ let free_glob_vars  =
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
   and vars_pattern bounded vs (loc,idl,p,c) =
-    let bounded' = List.fold_right Idset.add idl bounded  in
+    let bounded' = List.fold_right Id.Set.add idl bounded  in
     vars bounded' vs c
 
   and vars_option bounded vs = function None -> vs | Some p -> vars bounded vs p
@@ -222,8 +222,8 @@ let free_glob_vars  =
     vars_option bounded' vs tyopt
   in
   fun rt ->
-    let vs = vars Idset.empty Idset.empty rt in
-    Idset.elements vs
+    let vs = vars Id.Set.empty Id.Set.empty rt in
+    Id.Set.elements vs
 
 
 let loc_of_glob_constr = function
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index ed2d0ae2d..2e8908cfb 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -38,8 +38,8 @@ val map_glob_constr_left_to_right :
 
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
-val occur_glob_constr : identifier -> glob_constr -> bool
-val free_glob_vars : glob_constr -> identifier list
+val occur_glob_constr : Id.t -> glob_constr -> bool
+val free_glob_vars : glob_constr -> Id.t list
 val loc_of_glob_constr : glob_constr -> Loc.t
 
 (** Conversion from glob_constr to cases pattern, if possible
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 257ad448a..e42013b33 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -36,7 +36,7 @@ type recursion_scheme_error =
 exception RecursionSchemeError of recursion_scheme_error
 
 let make_prod_dep dep env = if dep then mkProd_name env else mkProd
-let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
+let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
 
 (*******************************************)
 (* Building curryfied elimination          *)
@@ -380,7 +380,7 @@ let mis_make_indrec env sigma listdepkind mib =
 	    let fixn = Array.of_list (List.rev ln) in
             let fixtyi = Array.of_list (List.rev ltyp) in
             let fixdef = Array.of_list (List.rev ldef) in
-            let names = Array.create nrec (Name(id_of_string "F")) in
+            let names = Array.create nrec (Name(Id.of_string "F")) in
 	      mkFix ((fixn,p),(names,fixtyi,fixdef))
       in
 	mrec 0 [] [] []
@@ -570,6 +570,6 @@ let lookup_eliminator ind_sp s =
     errorlabstrm "default_elim"
       (strbrk "Cannot find the elimination combinator " ++
        pr_id id ++ strbrk ", the elimination of the inductive definition " ++
-       pr_global_env Idset.empty (IndRef ind_sp) ++
+       pr_global_env Id.Set.empty (IndRef ind_sp) ++
        strbrk " on sort " ++ Termops.pr_sort_family s ++
        strbrk " is probably not allowed.")
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 1bf5fd90c..610a7bf39 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -63,6 +63,6 @@ val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types
 
 val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
-val make_elimination_ident : identifier -> sorts_family -> identifier
+val make_elimination_ident : Id.t -> sorts_family -> Id.t
 
 val case_suffix : string
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index bd4df6edd..ddf615033 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -34,5 +34,5 @@ val is_nowhere : 'a clause_expr -> bool
 
 (** Clause conversion functions, parametrized by a hyp enumeration function *)
 
-val simple_clause_of : (unit -> identifier list) -> clause -> simple_clause
-val concrete_clause_of : (unit -> identifier list) -> clause -> concrete_clause
+val simple_clause_of : (unit -> Id.t list) -> clause -> simple_clause
+val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 9f4badd22..dfc52295d 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -43,14 +43,14 @@ open Misctypes
 
  *)
 
-type bound_ident_map = (identifier * identifier) list
+type bound_ident_map = (Id.t * Id.t) list
 
 exception PatternMatchingFailure
 
 let constrain n (ids, m as x) (names, terms as subst) =
   try
     let (ids',m') = List.assoc n terms in
-    if List.equal id_eq ids ids' && eq_constr m m' then subst
+    if List.equal Id.equal ids ids' && eq_constr m m' then subst
     else raise PatternMatchingFailure
   with
       Not_found ->
@@ -89,7 +89,7 @@ let build_lambda toabstract stk (m : constr) =
 let rec list_insert a = function
 | [] -> [a]
 | b :: l ->
-  let ord = id_ord a b in
+  let ord = Id.compare a b in
   if ord < 0 then a :: b :: l
   else if ord > 0 then b :: list_insert a l
   else raise PatternMatchingFailure
@@ -162,9 +162,9 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 
       | PMeta None, m -> subst
 
-      | PRef (VarRef v1), Var v2 when id_eq v1 v2 -> subst
+      | PRef (VarRef v1), Var v2 when Id.equal v1 v2 -> subst
 
-      | PVar v1, Var v2 when id_eq v1 v2 -> subst
+      | PVar v1, Var v2 when Id.equal v1 v2 -> subst
 
       | PRef ref, _ when conv (constr_of_global ref) cT -> subst
 
@@ -249,7 +249,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 
   in
   let names,terms = sorec [] ([],[]) pat c in
-  (names, List.sort (fun (a, _) (b, _) -> id_ord a b) terms)
+  (names, List.sort (fun (a, _) (b, _) -> Id.compare a b) terms)
 
 let matches_core_closed convert allow_partial_app pat c =
   let names,subst = matches_core convert allow_partial_app false pat c in
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 273c4d061..05e01e2e2 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -25,7 +25,7 @@ val special_meta : metavariable
 (** [bound_ident_map] represents the result of matching binding
    identifiers of the pattern with the binding identifiers of the term
    matched *)
-type bound_ident_map = (identifier * identifier) list
+type bound_ident_map = (Id.t * Id.t) list
 
 (** [matches pat c] matches [c] against [pat] and returns the resulting
    assignment of metavariables; it raises [PatternMatchingFailure] if
diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml
index c7f51d17b..5e725979b 100644
--- a/pretyping/namegen.ml
+++ b/pretyping/namegen.ml
@@ -63,7 +63,7 @@ let is_constructor id =
 (* Generating "intuitive" names from its type *)
 
 let lowercase_first_char id = (* First character of a constr *)
-  Unicode.lowercase_first_char (string_of_id id)
+  Unicode.lowercase_first_char (Id.to_string id)
 
 let sort_hdchar = function
   | Prop(_) -> "P"
@@ -100,11 +100,11 @@ let hdchar env c =
   hdrec 0 c
 
 let id_of_name_using_hdchar env a = function
-  | Anonymous -> id_of_string (hdchar env a)
+  | Anonymous -> Id.of_string (hdchar env a)
   | Name id   -> id
 
 let named_hd env a = function
-  | Anonymous -> Name (id_of_string (hdchar env a))
+  | Anonymous -> Name (Id.of_string (hdchar env a))
   | x         -> x
 
 let mkProd_name   env (n,a,b) = mkProd (named_hd env a n, a, b)
@@ -139,7 +139,7 @@ let it_mkLambda_or_LetIn_name env b hyps =
 (**********************************************************************)
 (* Fresh names *)
 
-let default_x = id_of_string "x"
+let default_x = Id.of_string "x"
 
 (* Looks for next "good" name by lifting subscript *)
 
@@ -179,7 +179,7 @@ let next_ident_away_in_goal id avoid =
   next_ident_away_from id bad
 
 let next_name_away_in_goal na avoid =
-  let id = match na with Name id -> id | Anonymous -> id_of_string "H" in
+  let id = match na with Name id -> id | Anonymous -> Id.of_string "H" in
   next_ident_away_in_goal id avoid
 
 (* 3- Looks for next fresh name outside a list that is moreover valid
@@ -203,7 +203,7 @@ let next_ident_away id avoid =
   else id
 
 let next_name_away_with_default default na avoid =
-  let id = match na with Name id -> id | Anonymous -> id_of_string default in
+  let id = match na with Name id -> id | Anonymous -> Id.of_string default in
   next_ident_away id avoid
 
 let reserved_type_name = ref (fun t -> Anonymous)
@@ -214,7 +214,7 @@ let next_name_away_with_default_using_types default na avoid t =
     | Name id -> id
     | Anonymous -> match !reserved_type_name t with
 	| Name id -> id
-	| Anonymous -> id_of_string default in
+	| Anonymous -> Id.of_string default in
   next_ident_away id avoid
 
 let next_name_away = next_name_away_with_default "H"
@@ -237,7 +237,7 @@ let occur_rel p env id =
   try
     let name = lookup_name_of_rel p env in
     begin match name with
-    | Name id' -> id_eq id' id
+    | Name id' -> Id.equal id' id
     | Anonymous -> false
     end
   with Not_found -> false (* Unbound indice : may happen in debug *)
@@ -246,7 +246,7 @@ let visibly_occur_id id (nenv,c) =
   let rec occur n c = match kind_of_term c with
     | Const _ | Ind _ | Construct _ | Var _
       when
-        let short = shortest_qualid_of_global Idset.empty (global_of_constr c) in
+        let short = shortest_qualid_of_global Id.Set.empty (global_of_constr c) in
         qualid_eq short (qualid_of_ident id) ->
       raise Occur
     | Rel p when p>n & occur_rel (p-n) nenv id -> raise Occur
@@ -267,7 +267,7 @@ let next_name_away_for_default_printing env_t na avoid =
       (* In principle, an anonymous name is not dependent and will not be *)
       (* taken into account by the function compute_displayed_name_in; *)
       (* just in case, invent a valid name *)
-      id_of_string "H" in
+      Id.of_string "H" in
   next_ident_away_for_default_printing env_t id avoid
 
 (**********************************************************************)
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index e23c6dad8..6702c9f70 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.mli
@@ -13,10 +13,10 @@ open Environ
 (*********************************************************************
    Generating "intuitive" names from their type *)
 
-val lowercase_first_char : identifier -> string
+val lowercase_first_char : Id.t -> string
 val sort_hdchar : sorts -> string
 val hdchar : env -> types -> string
-val id_of_name_using_hdchar : env -> types -> name -> identifier
+val id_of_name_using_hdchar : env -> types -> name -> Id.t
 val named_hd : env -> types -> name -> name
 
 val mkProd_name : env -> name * types * types -> types
@@ -40,27 +40,27 @@ val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
    Fresh names *)
 
 (** Avoid clashing with a name satisfying some predicate *)
-val next_ident_away_from : identifier -> (identifier -> bool) -> identifier
+val next_ident_away_from : Id.t -> (Id.t -> bool) -> Id.t
 
 (** Avoid clashing with a name of the given list *)
-val next_ident_away : identifier -> identifier list -> identifier
+val next_ident_away : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a name already used in current module *)
-val next_ident_away_in_goal : identifier -> identifier list -> identifier
+val next_ident_away_in_goal : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a name already used in current module 
    but tolerate overwriting section variables, as in goals *)
-val next_global_ident_away : identifier -> identifier list -> identifier
+val next_global_ident_away : Id.t -> Id.t list -> Id.t
 
 (** Avoid clashing with a constructor name already used in current module *)
-val next_name_away_in_cases_pattern : name -> identifier list -> identifier
+val next_name_away_in_cases_pattern : name -> Id.t list -> Id.t
 
-val next_name_away  : name -> identifier list -> identifier (** default is "H" *)
-val next_name_away_with_default : string -> name -> identifier list ->
-  identifier
+val next_name_away  : name -> Id.t list -> Id.t (** default is "H" *)
+val next_name_away_with_default : string -> name -> Id.t list ->
+  Id.t
 
 val next_name_away_with_default_using_types : string -> name ->
-  identifier list -> types -> identifier
+  Id.t list -> types -> Id.t
 
 val set_reserved_typed_name : (types -> name) -> unit
 
@@ -75,10 +75,10 @@ type renaming_flags =
 val make_all_name_different : env -> env
 
 val compute_displayed_name_in :
-  renaming_flags -> identifier list -> name -> constr -> name * identifier list
+  renaming_flags -> Id.t list -> name -> constr -> name * Id.t list
 val compute_and_force_displayed_name_in :
-  renaming_flags -> identifier list -> name -> constr -> name * identifier list
+  renaming_flags -> Id.t list -> name -> constr -> name * Id.t list
 val compute_displayed_let_name_in :
-  renaming_flags -> identifier list -> name -> constr -> name * identifier list
+  renaming_flags -> Id.t list -> name -> constr -> name * Id.t list
 val rename_bound_vars_as_displayed :
-  identifier list -> name list -> types -> types
+  Id.t list -> name list -> types -> types
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index c7819e134..d784fc0ed 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -29,7 +29,7 @@ let case_info_pattern_eq i1 i2 =
 
 let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PRef r1, PRef r2 -> eq_gr r1 r2
-| PVar v1, PVar v2 -> id_eq v1 v2
+| PVar v1, PVar v2 -> Id.equal v1 v2
 | PEvar (ev1, ctx1), PEvar (ev2, ctx2) ->
   Int.equal ev1 ev2 && Array.equal constr_pattern_eq ctx1 ctx2
 | PRel i1, PRel i2 ->
@@ -37,7 +37,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PApp (t1, arg1), PApp (t2, arg2) ->
   constr_pattern_eq t1 t2 && Array.equal constr_pattern_eq arg1 arg2
 | PSoApp (id1, arg1), PSoApp (id2, arg2) ->
-  id_eq id1 id2 && List.equal constr_pattern_eq arg1 arg2
+  Id.equal id1 id2 && List.equal constr_pattern_eq arg1 arg2
 | PLambda (v1, t1, b1), PLambda (v2, t2, b2) ->
   name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PProd (v1, t1, b1), PProd (v2, t2, b2) ->
@@ -45,7 +45,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
 | PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
   name_eq v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PSort s1, PSort s2 -> glob_sort_eq s1 s2
-| PMeta m1, PMeta m2 -> Option.equal id_eq m1 m2
+| PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
   constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
 | PCase (info1, p1, r1, l1), PCase (info2, p2, r2, l2) ->
@@ -122,7 +122,7 @@ let pattern_of_constr sigma t =
   let rec pattern_of_constr t =
   match kind_of_term t with
     | Rel n  -> PRel n
-    | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
+    | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
     | Sort (Prop Null) -> PSort GProp
     | Sort (Prop Pos) -> PSort GSet
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index b20510b86..8148fe25d 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -53,7 +53,7 @@ val pattern_of_glob_constr : glob_constr ->
       patvar list * constr_pattern
 
 val instantiate_pattern :
-  Evd.evar_map -> (identifier * (identifier list * constr)) list ->
+  Evd.evar_map -> (Id.t * (Id.t list * constr)) list ->
   constr_pattern -> constr_pattern
 
 val lift_pattern : int -> constr_pattern -> constr_pattern
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 0cd5743cd..cced783f5 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -26,13 +26,13 @@ type pretype_error =
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
-  | NoOccurrenceFound of constr * identifier option
+  | NoOccurrenceFound of constr * Id.t option
   | CannotFindWellTypedAbstraction of constr * constr list
   | WrongAbstractionType of name * constr * types * types
   | AbstractionOverMeta of name * name
   | NonLinearUnification of name * constr
   (* Pretyping *)
-  | VarNotFound of identifier
+  | VarNotFound of Id.t
   | UnexpectedType of constr * constr
   | NotProduct of constr
   | TypingError of type_error
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e2e66e80f..aa0b65e4f 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -28,13 +28,13 @@ type pretype_error =
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
-  | NoOccurrenceFound of constr * identifier option
+  | NoOccurrenceFound of constr * Id.t option
   | CannotFindWellTypedAbstraction of constr * constr list
   | WrongAbstractionType of name * constr * types * types
   | AbstractionOverMeta of name * name
   | NonLinearUnification of name * constr
   (** Pretyping *)
-  | VarNotFound of identifier
+  | VarNotFound of Id.t
   | UnexpectedType of constr * constr
   | NotProduct of constr
   | TypingError of Type_errors.type_error
@@ -131,4 +131,4 @@ val error_not_product_loc :
 
 (** {6 Error in conversion from AST to glob_constr } *)
 
-val error_var_not_found_loc : Loc.t -> identifier -> 'b
+val error_var_not_found_loc : Loc.t -> Id.t -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 674c7e19e..358d53e48 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,8 +44,8 @@ open Pattern
 open Misctypes
 
 type typing_constraint = OfType of types option | IsType
-type var_map = (identifier * constr_under_binders) list
-type unbound_ltac_var_map = (identifier * identifier option) list
+type var_map = (Id.t * constr_under_binders) list
+type unbound_ltac_var_map = (Id.t * Id.t option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
@@ -609,7 +609,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 		(fun (n, b, t) ->
 		   match n with
                    Name _ -> (n, b, t)
-                   | Anonymous -> (Name (id_of_string "H"), b, t))
+                   | Anonymous -> (Name (Id.of_string "H"), b, t))
 		cs.cs_args
 	  in
 	  let env_c = push_rel_context csgn env in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index ec1cc0c6d..e637d2b8e 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -28,8 +28,8 @@ val search_guard :
 
 type typing_constraint = OfType of types option | IsType
 
-type var_map = (identifier * Pattern.constr_under_binders) list
-type unbound_ltac_var_map = (identifier * identifier option) list
+type var_map = (Id.t * Pattern.constr_under_binders) list
+type unbound_ltac_var_map = (Id.t * Id.t option) list
 type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
diff --git a/pretyping/program.ml b/pretyping/program.ml
index a8e91856b..a0befa130 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -11,10 +11,10 @@ open Util
 open Names
 open Term
 
-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 find_reference locstr dir s =
-  let sp = Libnames.make_path (make_dir dir) (id_of_string s) in
+  let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
   try Nametab.global_of_path sp
   with Not_found -> anomaly (locstr^": cannot find "^(Libnames.string_of_path sp))
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 23de3eb19..72d43fabd 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -243,8 +243,8 @@ let compute_canonical_projections (con,ind) =
 		     ((ConstRef proji_sp, patt, n, args) :: l)
 		 with Not_found ->
                    if Flags.is_verbose () then
-                     (let con_pp = Nametab.pr_global_env Idset.empty (ConstRef con)
-                      and proji_sp_pp = Nametab.pr_global_env Idset.empty (ConstRef proji_sp) in
+                     (let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con)
+                      and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in
 		      msg_warning (strbrk "No global reference exists for projection value"
                                    ++ Termops.print_constr t ++ strbrk " in instance "  
                                    ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it."));
@@ -259,7 +259,7 @@ let compute_canonical_projections (con,ind) =
     comp
 
 let pr_cs_pattern = function
-    Const_cs c -> Nametab.pr_global_env Idset.empty c
+    Const_cs c -> Nametab.pr_global_env Id.Set.empty c
   | Prod_cs -> str "_ -> _"
   | Default_cs -> str "_"
   | Sort_cs s -> Termops.pr_sort_family s
@@ -277,7 +277,7 @@ let open_canonical_structure i (_,o) =
             if Flags.is_verbose () then
               let old_can_s = (Termops.print_constr cs.o_DEF)
               and new_can_s = (Termops.print_constr s.o_DEF) in
-              let prj = (Nametab.pr_global_env Idset.empty proj)
+              let prj = (Nametab.pr_global_env Id.Set.empty proj)
               and hd_val = (pr_cs_pattern cs_pat) in
               msg_warning (strbrk "Ignoring canonical projection to " ++ hd_val
                              ++ strbrk " by " ++ prj ++ strbrk " in "
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index de23de75f..f2366ea02 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -644,7 +644,7 @@ let plain_instance s c =
 	    (try let g = List.assoc p s in
 	    match kind_of_term g with
             | App _ ->
-                let h = id_of_string "H" in
+                let h = Id.of_string "H" in
                 mkLetIn (Name h,g,t,mkApp(mkRel 1,Array.map (lift 1) l'))
             | _ -> mkApp (g,l')
 	    with Not_found -> mkApp (f,l'))
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 800945f02..beb0be32f 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -40,7 +40,7 @@ let sort_of_atomic_type env sigma ft args =
 let type_of_var env id =
   try let (_,_,ty) = lookup_named id env in ty
   with Not_found ->
-    anomaly ("type_of: variable "^(string_of_id id)^" unbound")
+    anomaly ("type_of: variable "^(Id.to_string id)^" unbound")
 
 let is_impredicative_set env = match Environ.engagement env with
 | Some ImpredicativeSet -> true
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 6c2f8f189..1a4bd3877 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -38,7 +38,7 @@ exception Redelimination
 
 let error_not_evaluable r =
   errorlabstrm "error_not_evaluable"
-    (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Idset.empty r ++
+    (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++
      spc () ++ str "to an evaluable reference.")
 
 let is_evaluable_const env cst =
@@ -70,13 +70,13 @@ let global_of_evaluable_reference = function
 
 type evaluable_reference =
   | EvalConst of constant
-  | EvalVar of identifier
+  | EvalVar of Id.t
   | EvalRel of int
   | EvalEvar of existential
 
 let evaluable_reference_eq r1 r2 = match r1, r2 with
 | EvalConst c1, EvalConst c2 -> eq_constant c1 c2
-| EvalVar id1, EvalVar id2 -> id_eq id1 id2
+| EvalVar id1, EvalVar id2 -> Id.equal id1 id2
 | EvalRel i1, EvalRel i2 -> Int.equal i1 i2
 | EvalEvar (e1, ctx1), EvalEvar (e2, ctx2) ->
   Int.equal e1 e2 && Array.equal eq_constr ctx1 ctx2
@@ -220,7 +220,7 @@ let invert_name labs l na0 env sigma ref = function
   | Name id ->
       let minfxargs = List.length l in
       begin match na0 with
-      | Name id' when id_eq id' id ->
+      | Name id' when Id.equal id' id ->
         Some (minfxargs,ref)
       | _ ->
 	let refi = match ref with
@@ -334,7 +334,7 @@ let reference_eval sigma env = function
    The type Tij' is Tij[yi(j-1)..y1 <- ai(j-1)..a1]
 *)
 
-let x = Name (id_of_string "x")
+let x = Name (Id.of_string "x")
 
 let make_elim_fun (names,(nbfix,lv,n)) largs =
   let lu = List.firstn n largs in
@@ -363,8 +363,8 @@ let make_elim_fun (names,(nbfix,lv,n)) largs =
    do so that the reduction uses this extra information *)
 
 let dummy = mkProp
-let vfx = id_of_string"_expanded_fix_"
-let vfun = id_of_string"_eliminator_function_"
+let vfx = Id.of_string"_expanded_fix_"
+let vfun = Id.of_string"_eliminator_function_"
 
 (* Mark every occurrence of substituted vars (associated to a function)
    as a problem variable: an evar that can be instantiated either by
@@ -957,7 +957,7 @@ let substlin env evalref n (nowhere_except_in,locs) c =
   (!pos, t')
 
 let string_of_evaluable_ref env = function
-  | EvalVarRef id -> string_of_id id
+  | EvalVarRef id -> Id.to_string id
   | EvalConstRef kn ->
       string_of_qualid
         (Nametab.shortest_qualid_of_global (vars_of_env env) (ConstRef kn))
@@ -1125,7 +1125,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
     | IndRef mind' when eq_ind mind mind' -> t
     | _ ->
       errorlabstrm "" (str "Cannot recognize a statement based on " ++
-        Nametab.pr_global_env Idset.empty ref ++ str".")
+        Nametab.pr_global_env Id.Set.empty ref ++ str".")
     end
   else
   (* lazily reduces to match the head of [t] with the expected [ref] *)
@@ -1138,7 +1138,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
 	  else
 	     errorlabstrm ""
 	       (str "Cannot recognize an atomic statement based on " ++
-	        Nametab.pr_global_env Idset.empty ref ++ str".")
+	        Nametab.pr_global_env Id.Set.empty ref ++ str".")
       | _ ->
 	  try
 	    if eq_gr (global_of_constr c) ref
@@ -1151,7 +1151,7 @@ let reduce_to_ref_gen allow_product env sigma ref t =
           with NotStepReducible ->
 	    errorlabstrm ""
 	      (str "Cannot recognize a statement based on " ++
-	       Nametab.pr_global_env Idset.empty ref ++ str".")
+	       Nametab.pr_global_env Id.Set.empty ref ++ str".")
   in
   elimrec env t []
 
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 4a267dd7e..2cc538004 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -221,7 +221,7 @@ let lookup_rel_id id sign =
     | []                     -> raise Not_found
     | (Anonymous, _, _) :: l -> lookrec (n + 1) l
     | (Name id', b, t) :: l  ->
-      if Int.equal (Names.id_ord id' id) 0 then (n, b, t) else lookrec (n + 1) l
+      if Int.equal (Names.Id.compare id' id) 0 then (n, b, t) else lookrec (n + 1) l
   in
   lookrec 1 sign
 
@@ -564,9 +564,9 @@ let collect_metas c =
    all section variables; for the latter, use global_vars_set *)
 let collect_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
   | _ -> fold_constr aux vars c in
-  aux Idset.empty c
+  aux Id.Set.empty c
 
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
@@ -726,7 +726,7 @@ type 'a testing_function = {
   match_fun : constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
-  mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
+  mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option
 }
 
 let subst_closed_term_occ_gen_modulo occs test cl occ t =
@@ -825,14 +825,14 @@ let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d =
 
 let vars_of_env env =
   let s =
-    Sign.fold_named_context (fun (id,_,_) s -> Idset.add id s)
-      (named_context env) ~init:Idset.empty in
+    Sign.fold_named_context (fun (id,_,_) s -> Id.Set.add id s)
+      (named_context env) ~init:Id.Set.empty in
   Sign.fold_rel_context
-    (fun (na,_,_) s -> match na with Name id -> Idset.add id s | _ -> s)
+    (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s
 
 let add_vname vars = function
-    Name id -> Idset.add id vars
+    Name id -> Id.Set.add id vars
   | _ -> vars
 
 (*************************)
@@ -846,7 +846,7 @@ let lookup_name_of_rel p names =
 let lookup_rel_of_name id names =
   let rec lookrec n = function
     | Anonymous :: l  -> lookrec (n+1) l
-    | (Name id') :: l -> if id_eq id' id then n else lookrec (n+1) l
+    | (Name id') :: l -> if Id.equal id' id then n else lookrec (n+1) l
     | []            -> raise Not_found
   in
   lookrec 1 names
@@ -1049,31 +1049,31 @@ let adjust_subst_to_rel_context sign l =
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let rec mem_named_context id = function
-  | (id',_,_) :: _ when id_eq id id' -> true
+  | (id',_,_) :: _ when Id.equal id id' -> true
   | _ :: sign -> mem_named_context id sign
   | [] -> false
 
 let clear_named_body id env =
   let aux _ = function
-  | (id',Some c,t) when id_eq id id' -> push_named (id,None,t)
+  | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t)
   | d -> push_named d in
   fold_named_context aux env ~init:(reset_context env)
 
-let global_vars env ids = Idset.elements (global_vars_set env ids)
+let global_vars env ids = Id.Set.elements (global_vars_set env ids)
 
 let global_vars_set_of_decl env = function
   | (_,None,t) -> global_vars_set env t
   | (_,Some c,t) ->
-      Idset.union (global_vars_set env t)
+      Id.Set.union (global_vars_set env t)
         (global_vars_set env c)
 
 let dependency_closure env sign hyps =
-  if Idset.is_empty hyps then [] else
+  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 hs then
-            (Idset.union (global_vars_set_of_decl env d) (Idset.remove x hs),
+          if Id.Set.mem x hs then
+            (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
             x::hl)
           else (hs,hl))
         ~init:(hyps,[])
@@ -1111,8 +1111,8 @@ let impossible_default_case = ref None
 let set_impossible_default_clause c = impossible_default_case := Some c
 
 let coq_unit_judge =
-  let na1 = Name (id_of_string "A") in
-  let na2 = Name (id_of_string "H") in
+  let na1 = Name (Id.of_string "A") in
+  let na2 = Name (Id.of_string "H") in
   fun () ->
     match !impossible_default_case with
     | Some (id,type_of_id) ->
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 096cdbcbb..051a77883 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -41,7 +41,7 @@ val push_rel_assum : name * types -> env -> env
 val push_rels_assum : (name * types) list -> env -> env
 val push_named_rec_types : name array * types array * 'a -> env -> env
 
-val lookup_rel_id : identifier -> rel_context -> int * constr option * types
+val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
 (** Associates the contents of an identifier in a [rel_context]. Raise
     [Not_found] if there is no such identifier. *)
 
@@ -104,16 +104,16 @@ val occur_meta : types -> bool
 val occur_existential : types -> bool
 val occur_meta_or_existential : types -> bool
 val occur_evar : existential_key -> types -> bool
-val occur_var : env -> identifier -> types -> bool
+val occur_var : env -> Id.t -> types -> bool
 val occur_var_in_decl :
   env ->
-  identifier -> 'a * types option * types -> bool
+  Id.t -> 'a * types option * types -> bool
 val free_rels : constr -> Int.Set.t
 val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val count_occurrences : constr -> constr -> int
 val collect_metas : constr -> int list
-val collect_vars : constr -> Idset.t (** for visible vars only *)
+val collect_vars : constr -> Id.Set.t (** for visible vars only *)
 val occur_term : constr -> constr -> bool (** Synonymous
  of dependent 
    Substitution of metavariables *)
@@ -162,7 +162,7 @@ type 'a testing_function = {
   match_fun : constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
   mutable testing_state : 'a;
-  mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
+  mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option
 }
 
 val make_eq_test : constr -> unit testing_function
@@ -170,7 +170,7 @@ val make_eq_test : constr -> unit testing_function
 exception NotUnifiable
 
 val subst_closed_term_occ_modulo :
-  occurrences -> 'a testing_function -> (identifier * hyp_location_flag) option
+  occurrences -> 'a testing_function -> (Id.t * hyp_location_flag) option
   -> constr -> types
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at
@@ -228,19 +228,19 @@ val adjust_app_array_size : constr -> constr array -> constr -> constr array ->
 type names_context = name list
 val add_name : name -> names_context -> names_context
 val lookup_name_of_rel : int -> names_context -> name
-val lookup_rel_of_name : identifier -> names_context -> int
+val lookup_rel_of_name : Id.t -> names_context -> int
 val empty_names_context : names_context
-val ids_of_rel_context : rel_context -> identifier list
-val ids_of_named_context : named_context -> identifier list
-val ids_of_context : env -> identifier list
+val ids_of_rel_context : rel_context -> Id.t list
+val ids_of_named_context : named_context -> Id.t list
+val ids_of_context : env -> Id.t list
 val names_of_rel_context : env -> names_context
 
 val context_chop : int -> rel_context -> rel_context * rel_context
 val env_rel_context_chop : int -> env -> env * rel_context
 
 (** Set of local names *)
-val vars_of_env: env -> Idset.t
-val add_vname : Idset.t -> name -> Idset.t
+val vars_of_env: env -> Id.Set.t
+val add_vname : Id.Set.t -> name -> Id.Set.t
 
 (** other signature iterators *)
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
@@ -256,19 +256,19 @@ val map_rel_context_with_binders :
 val fold_named_context_both_sides :
   ('a -> named_declaration -> named_declaration list -> 'a) ->
     named_context -> init:'a -> 'a
-val mem_named_context : identifier -> named_context -> bool
+val mem_named_context : Id.t -> named_context -> bool
 
-val clear_named_body : identifier -> env -> env
+val clear_named_body : Id.t -> env -> env
 
-val global_vars : env -> constr -> identifier list
-val global_vars_set_of_decl : env -> named_declaration -> Idset.t
+val global_vars : env -> constr -> Id.t list
+val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
-val dependency_closure : env -> named_context -> Idset.t -> identifier list
+val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list
 
 (** Test if an identifier is the basename of a global reference *)
-val is_section_variable : identifier -> bool
+val is_section_variable : Id.t -> bool
 
 val isGlobalRef : constr -> bool
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 4a0b66a7b..cfcf9cf43 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -19,8 +19,8 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
     | NotAClass of constr
-    | UnboundMethod of global_reference * identifier Loc.located (* Class name, method *)
-    | NoInstance of identifier Loc.located * constr list
+    | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
+    | NoInstance of Id.t Loc.located * constr list
     | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
     | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index ea72eab72..5155b7163 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -23,8 +23,8 @@ type contexts = Parameters | Properties
 
 type typeclass_error =
   | NotAClass of constr
-  | UnboundMethod of global_reference * identifier located (** Class name, method *)
-  | NoInstance of identifier located * constr list
+  | UnboundMethod of global_reference * Id.t located (** Class name, method *)
+  | NoInstance of Id.t located * constr list
   | UnsatisfiableConstraints of evar_map * (existential_key * Evar_kinds.t) option
   | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
 
@@ -32,9 +32,9 @@ exception TypeClassError of env * typeclass_error
 
 val not_a_class : env -> constr -> 'a
 
-val unbound_method : env -> global_reference -> identifier located -> 'a
+val unbound_method : env -> global_reference -> Id.t located -> 'a
 
-val no_instance : env -> identifier located -> constr list -> 'a
+val no_instance : env -> Id.t located -> constr list -> 'a
 
 val unsatisfiable_constraints : env -> evar_map -> evar option -> 'a
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index facc243e2..dee597733 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -337,7 +337,7 @@ let key_of b flags f =
         Cpred.mem cst (snd flags.modulo_delta) ->
       Some (ConstKey cst)
   | Var id when is_transparent (VarKey id) &&
-        Idpred.mem id (fst flags.modulo_delta) ->
+        Id.Pred.mem id (fst flags.modulo_delta) ->
       Some (VarKey id)
   | _ -> None
 
@@ -657,9 +657,9 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
       | _ -> constr_cmp cv_pb m n) then true
       else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
             | Some (cv_id, cv_k), (dl_id, dl_k) ->
-                Idpred.subset dl_id cv_id && Cpred.subset dl_k cv_k
+                Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
             | None,(dl_id, dl_k) ->
-                Idpred.is_empty dl_id && Cpred.is_empty dl_k)
+                Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
       then error_cannot_unify env sigma (m, n) else false)
     then subst
     else unirec_rec (env,0) cv_pb conv_at_top false subst m n
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 321364140..82eccab96 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -22,7 +22,7 @@ let crazy_type =  mkSet
 
 let decompose_prod env t =
   let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
-  if name = Anonymous then (Name (id_of_string "x"),dom,codom)
+  if name = Anonymous then (Name (Id.of_string "x"),dom,codom)
   else res
 
 exception Find_at of int
@@ -141,7 +141,7 @@ and nf_whd env whd typ =
   | Vsort s -> mkSort s
   | Vprod p ->
       let dom = nf_vtype env (dom p) in
-      let name = Name (id_of_string "x") in
+      let name = Name (Id.of_string "x") in
       let vc = body_of_vfun (nb_rel env) (codom p) in
       let codom = nf_vtype (push_rel (name,None,dom) env) vc  in
       mkProd(name,dom,codom)
@@ -213,7 +213,7 @@ and nf_predicate env ind mip params v pT =
   | Vfun f, _ ->
       let k = nb_rel env in
       let vb = body_of_vfun k f in
-      let name = Name (id_of_string "c") in
+      let name = Name (Id.of_string "c") in
       let n = mip.mind_nrealargs in
       let rargs = Array.init n (fun i -> mkRel (n-i)) in
       let params = if n=0 then params else Array.map (lift n) params in
@@ -262,7 +262,7 @@ and nf_fix env f =
   let vb, vt = reduce_fix k f in
   let ndef = Array.length vt in
   let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
-  let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in
+  let name = Array.init ndef (fun _ -> (Name (Id.of_string "Ffix"))) in
   let env = push_rec_types (name,ft,ft) env in
   let fb = Util.Array.map2 (fun v t -> nf_fun env v t) vb ft in
   mkFix ((rec_args,init),(name,ft,fb))
@@ -280,7 +280,7 @@ and nf_cofix env cf =
   let vb,vt = reduce_cofix k cf in
   let ndef = Array.length vt in
   let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
-  let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in
+  let name = Array.init ndef (fun _ -> (Name (Id.of_string "Fcofix"))) in
   let env = push_rec_types (name,cft,cft) env in
   let cfb = Util.Array.map2 (fun v t -> nf_val env v t) vb cft in
   mkCoFix (init,(name,cft,cfb))