Modulification of identifier

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

22 files changed, 220 insertions, 220 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index d49219114..602c2314a 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -53,9 +53,9 @@ let prim_token_eq t1 t2 = match t1, t2 with
 
 let explicitation_eq ex1 ex2 = match ex1, ex2 with
 | ExplByPos (i1, id1), ExplByPos (i2, id2) ->
-  Int.equal i1 i2 && Option.equal id_eq id1 id2
+  Int.equal i1 i2 && Option.equal Id.equal id1 id2
 | ExplByName id1, ExplByName id2 ->
-  id_eq id1 id2
+  Id.equal id1 id2
 | _ -> false
 
 let eq_located f (_, x) (_, y) = f x y
@@ -64,7 +64,7 @@ let rec cases_pattern_expr_eq p1 p2 =
   if p1 == p2 then true
   else match p1, p2 with
   | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) ->
-      id_eq i1 i2 && cases_pattern_expr_eq a1 a2
+      Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
       eq_reference c1 c2 &&
       List.equal cases_pattern_expr_eq a1 a2 &&
@@ -97,10 +97,10 @@ let rec constr_expr_eq e1 e2 =
   else match e1, e2 with
   | CRef r1, CRef r2 -> eq_reference r1 r2
   | CFix(_,id1,fl1), CFix(_,id2,fl2) ->
-      eq_located id_eq id1 id2 &&
+      eq_located Id.equal id1 id2 &&
       List.equal fix_expr_eq fl1 fl2
   | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) ->
-      eq_located id_eq id1 id2 &&
+      eq_located Id.equal id1 id2 &&
       List.equal cofix_expr_eq fl1 fl2
   | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
       List.equal binder_expr_eq bl1 bl2 &&
@@ -145,7 +145,7 @@ let rec constr_expr_eq e1 e2 =
     constr_expr_eq f1 f2
   | CHole _, CHole _ -> true
   | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) ->
-    (b1 : bool) == b2 && id_eq i1 i2
+    (b1 : bool) == b2 && Id.equal i1 i2
   | CEvar (_, ev1, c1), CEvar (_, ev2, c2) ->
     Int.equal ev1 ev2 &&
     Option.equal (List.equal constr_expr_eq) c1 c2
@@ -188,15 +188,15 @@ and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
   List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2
 
 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
-  (eq_located id_eq id1 id2) &&
-  Option.equal (eq_located id_eq) j1 j2 &&
+  (eq_located Id.equal id1 id2) &&
+  Option.equal (eq_located Id.equal) j1 j2 &&
   recursion_order_expr_eq r1 r2 &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
 
 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
-  (eq_located id_eq id1 id2) &&
+  (eq_located Id.equal id1 id2) &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 8eb88f70d..49dea9f31 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -44,7 +44,7 @@ val local_binders_loc : local_binder list -> Loc.t
 
 (** {6 Constructors}*)
 
-val mkIdentC : identifier -> constr_expr
+val mkIdentC : Id.t -> constr_expr
 val mkRefC : reference -> constr_expr
 val mkAppC : constr_expr * constr_expr list -> constr_expr
 val mkCastC : constr_expr * constr_expr cast_type -> constr_expr
@@ -63,10 +63,10 @@ val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr
 
 (** {6 Destructors}*)
 
-val coerce_reference_to_id : reference -> identifier
+val coerce_reference_to_id : reference -> Id.t
 (** FIXME: nothing to do here *)
 
-val coerce_to_id : constr_expr -> identifier located
+val coerce_to_id : constr_expr -> Id.t located
 (** Destruct terms of the form [CRef (Ident _)]. *)
 
 val coerce_to_name : constr_expr -> name located
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d0be33031..c91db464d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -271,7 +271,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   match pat with
     | PatCstr(loc,cstrsp,args,na)
 	when !in_debugger||Inductiveops.mis_constructor_has_local_defs cstrsp ->
-      let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in
+      let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
       let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
       CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, [])
     | _ ->
@@ -308,12 +308,12 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
 		      | CPatAtom(_, None) :: tail -> ip q tail acc
 		    (* we don't want to have 'x = _' in our patterns *)
 		      | head :: tail -> ip q tail
-		        ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
+		        ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
 	      in
 	      CPatRecord(loc, List.rev (ip projs args []))
 	    with
 		Not_found | No_match | Exit ->
-                  let c = extern_reference loc Idset.empty (ConstructRef cstrsp) in
+                  let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in
 		  if !Topconstr.oldfashion_patterns then
 		    if pattern_printable_in_both_syntax cstrsp
 		    then CPatCstr (loc, c, [], args)
@@ -638,7 +638,7 @@ let rec extern inctx scopes vars r =
 				 | [] -> raise No_match
 				     (* we give up since the constructor is not complete *)
 				 | head :: tail -> ip q locs' tail
-				     ((extern_reference loc Idset.empty (ConstRef c), head) :: acc)
+				     ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
 		   in
 		 CRecord (loc, None, List.rev (ip projs locals args []))
 	       with
@@ -667,7 +667,7 @@ let rec extern inctx scopes vars r =
 
   | GCases (loc,sty,rtntypopt,tml,eqns) ->
     let vars' =
-      List.fold_right (name_fold Idset.add)
+      List.fold_right (name_fold Id.Set.add)
 	(cases_predicate_names tml) vars in
     let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
     let tml = List.map (fun (tm,(na,x)) ->
@@ -681,7 +681,7 @@ let rec extern inctx scopes vars r =
               else None
             end
         | Anonymous, _ -> None
-        | Name id, GVar (_,id') when id_eq id id' -> None
+        | Name id, GVar (_,id') when Id.equal id id' -> None
         | Name _, _ -> Some (Loc.ghost,na) in
       (sub_extern false scopes vars tm,
        (na',Option.map (fun (loc,ind,nal) ->
@@ -708,15 +708,15 @@ let rec extern inctx scopes vars r =
         sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
 
   | GRec (loc,fk,idv,blv,tyv,bv) ->
-      let vars' = Array.fold_right Idset.add idv vars in
+      let vars' = Array.fold_right Id.Set.add idv vars in
       (match fk with
 	 | GFix (nv,n) ->
 	     let listdecl =
 	       Array.mapi (fun i fi ->
                  let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
                  let (assums,ids,bl) = extern_local_binder scopes vars bl in
-                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
-                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+                 let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
 		 let n =
 		   match fst nv.(i) with
 		     | None -> None
@@ -731,8 +731,8 @@ let rec extern inctx scopes vars r =
 	     let listdecl =
                Array.mapi (fun i fi ->
                  let (_,ids,bl) = extern_local_binder scopes vars blv.(i) in
-                 let vars0 = List.fold_right (name_fold Idset.add) ids vars in
-                 let vars1 = List.fold_right (name_fold Idset.add) ids vars' in
+                 let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
+                 let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
 		 ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
                   sub_extern false scopes vars1 bv.(i))) idv
 	     in
@@ -775,13 +775,13 @@ and extern_local_binder scopes vars = function
     [] -> ([],[],[])
   | (na,bk,Some bd,ty)::l ->
       let (assums,ids,l) =
-        extern_local_binder scopes (name_fold Idset.add na vars) l in
+        extern_local_binder scopes (name_fold Id.Set.add na vars) l in
       (assums,na::ids,
        LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l)
 
   | (na,bk,None,ty)::l ->
       let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in
-      (match extern_local_binder scopes (name_fold Idset.add na vars) l with
+      (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
           (assums,ids,LocalRawAssum(nal,k,ty')::l)
             when constr_expr_eq ty ty' &
               match na with Name id -> not (occur_var_constr_expr id ty')
@@ -933,7 +933,7 @@ let rec glob_of_pat env = function
 	| Name id   -> id
 	| Anonymous ->
 	    anomaly "glob_constr_of_pattern: index to an anonymous variable"
-      with Not_found -> id_of_string ("_UNBOUND_REL_"^(string_of_int n)) in
+      with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar (loc,id)
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole)
   | PMeta (Some n) -> GPatVar (loc,(false,n))
@@ -976,7 +976,7 @@ let rec glob_of_pat env = function
   | PSort s -> GSort (loc,s)
 
 let extern_constr_pattern env pat =
-  extern true (None,[]) Idset.empty (glob_of_pat env pat)
+  extern true (None,[]) Id.Set.empty (glob_of_pat env pat)
 
 let extern_rel_context where env sign =
   let a = detype_rel_context where [] (names_of_rel_context env) sign in
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 0ca25656f..0e40e83e6 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -25,9 +25,9 @@ open Misctypes
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
    trees for printing *)
 
-val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
-val extern_glob_constr : Idset.t -> glob_constr -> constr_expr
-val extern_glob_type : Idset.t -> glob_constr -> constr_expr
+val extern_cases_pattern : Id.Set.t -> cases_pattern -> cases_pattern_expr
+val extern_glob_constr : Id.Set.t -> glob_constr -> constr_expr
+val extern_glob_type : Id.Set.t -> glob_constr -> constr_expr
 val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
 
 (** If [b=true] in [extern_constr b env c] then the variables in the first
@@ -35,7 +35,7 @@ val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
 
 val extern_constr : bool -> env -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
-val extern_reference : Loc.t -> Idset.t -> global_reference -> reference
+val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
 val extern_type : bool -> env -> types -> constr_expr
 val extern_sort : sorts -> glob_sort
 val extern_rel_context : constr option -> env ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index e4df61c47..f4fff70db 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -46,7 +46,7 @@ open Decl_kinds
    types and recursive definitions and of projection names in records *)
 
 type var_internalization_type =
-  | Inductive of identifier list (* list of params *)
+  | Inductive of Id.t list (* list of params *)
   | Recursive
   | Method
   | Variable
@@ -57,14 +57,14 @@ type var_internalization_data =
     var_internalization_type *
     (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
        in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
-    identifier list *
+    Id.t list *
     (* signature of impargs of the variable *)
     Impargs.implicit_status list *
     (* subscopes of the args of the variable *)
     scope_name option list
 
 type internalization_env =
-    (var_internalization_data) Idmap.t
+    (var_internalization_data) Id.Map.t
 
 type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
 
@@ -109,11 +109,11 @@ let global_reference_in_absolute_module dir id =
 (* Internalization errors                                             *)
 
 type internalization_error =
-  | VariableCapture of identifier * identifier
+  | VariableCapture of Id.t * Id.t
   | IllegalMetavariable
   | NotAConstructor of reference
-  | UnboundFixName of bool * identifier
-  | NonLinearPattern of identifier
+  | UnboundFixName of bool * Id.t
+  | NonLinearPattern of Id.t
   | BadPatternsNumber of int * int
 
 exception InternalizationError of Loc.t * internalization_error
@@ -165,7 +165,7 @@ let error_parameter_not_implicit loc =
 
 let parsing_explicit = ref false
 
-let empty_internalization_env = Idmap.empty
+let empty_internalization_env = Id.Map.empty
 
 let compute_explicitable_implicit imps = function
   | Inductive params ->
@@ -184,7 +184,7 @@ let compute_internalization_data env ty typ impl =
 
 let compute_internalization_env env ty =
   List.fold_left3
-    (fun map id typ impl -> Idmap.add id (compute_internalization_data env ty typ impl) map)
+    (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map)
     empty_internalization_env
 
 (**********************************************************************)
@@ -234,7 +234,7 @@ let contract_pat_notation ntn (l,ll) =
   !ntn',(l,ll)
 
 type intern_env = {
-  ids: Names.Idset.t;
+  ids: Names.Id.Set.t;
   unb: bool;
   tmp_scope: Notation_term.tmp_scope_name option;
   scopes: Notation_term.scope_name list;
@@ -354,14 +354,14 @@ let locate_if_isevar loc na = function
   | x -> x
 
 let reset_hidden_inductive_implicit_test env =
-  { env with impls = Idmap.fold (fun id x ->
+  { env with impls = Id.Map.fold (fun id x ->
        let x = match x with
          | (Inductive _,b,c,d) -> (Inductive [],b,c,d)
          | x -> x
-       in Idmap.add id x) env.impls Idmap.empty }
+       in Id.Map.add id x) env.impls Id.Map.empty }
 
 let check_hidden_implicit_parameters id impls =
-  if Idmap.exists (fun _ -> function
+  if Id.Map.exists (fun _ -> function
     | (Inductive indparams,_,_,_) -> List.mem id indparams
     | _ -> false) impls
   then
@@ -379,11 +379,11 @@ let push_name_env ?(global_level=false) lvar implargs env =
       set_var_scope loc id false env (let (_,ntnvars) = lvar in ntnvars);
       if global_level then Dumpglob.dump_definition (loc,id) true "var"
       else Dumpglob.dump_binding loc id;
-      {env with ids = Idset.add id env.ids; impls = Idmap.add id implargs env.impls}
+      {env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
 
 let intern_generalized_binder ?(global_level=false) intern_type lvar
     env (loc, na) b b' t ty =
-  let ids = (match na with Anonymous -> fun x -> x | Name na -> Idset.add na) env.ids in
+  let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in
   let ty, ids' =
     if t then ty, ids else
       Implicit_quantifiers.implicit_application ids
@@ -407,7 +407,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
 	    let id =
 	      match ty with
 	      | CApp (_, (_, CRef (Ident (loc,id))), _) -> id
-	      | _ -> id_of_string "H"
+	      | _ -> Id.of_string "H"
 	    in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
 	  in Name name
     | _ -> na
@@ -469,7 +469,7 @@ let intern_generalization intern env lvar loc bk ak c =
 (* Syntax extensions                                                  *)
 
 let option_mem_assoc id = function
-  | Some (id',c) -> id_eq id id'
+  | Some (id',c) -> Id.equal id id'
   | None -> false
 
 let find_fresh_name renaming (terms,termlists,binders) id =
@@ -477,7 +477,7 @@ let find_fresh_name renaming (terms,termlists,binders) id =
   let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) termlists) in
   let fvs3 = List.map snd renaming in
   (* TODO binders *)
-  let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in
+  let fvs = List.flatten (List.map Id.Set.elements (fvs1@fvs2)) @ fvs3 in
   next_ident_away id fvs
 
 let traverse_binder (terms,_,_ as subst)
@@ -488,12 +488,12 @@ let traverse_binder (terms,_,_ as subst)
   try
     (* Binders bound in the notation are considered first-order objects *)
     let _,na = coerce_to_name (fst (List.assoc id terms)) in
-    (renaming,{env with ids = name_fold Idset.add na env.ids}), na
+    (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na
   with Not_found ->
     (* Binders not bound in the notation do not capture variables *)
     (* outside the notation (i.e. in the substitution) *)
     let id' = find_fresh_name renaming subst id in
-    let renaming' = if id_eq id id' then renaming else (id,id')::renaming in
+    let renaming' = if Id.equal id id' then renaming else (id,id')::renaming in
     (renaming',env), Name id'
 
 let make_letins = List.fold_right (fun (loc,(na,b,t)) c -> GLetIn (loc,na,b,c))
@@ -510,7 +510,7 @@ let rec subordinate_letins letins = function
       letins,[]
 
 let rec subst_iterator y t = function
-  | GVar (_,id) as x -> if id_eq id y then t else x
+  | GVar (_,id) as x -> if Id.equal id y then t else x
   | x -> map_glob_constr (subst_iterator y t) x
 
 let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
@@ -607,15 +607,15 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   let (ltacvars,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let ty,expl_impls,impls,argsc = Idmap.find id genv.impls in
+    let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
     let expl_impls = List.map
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in
     let tys = string_of_ty ty in
-    Dumpglob.dump_reference loc "<>" (string_of_id id) tys;
+    Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
     GVar (loc,id), make_implicits_list impls, argsc, expl_impls
   with Not_found ->
   (* Is [id] bound in current term or is an ltac var bound to constr *)
-  if Idset.mem id genv.ids or List.mem id ltacvars
+  if Id.Set.mem id genv.ids or List.mem id ltacvars
   then
     GVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
@@ -624,7 +624,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
   then
     (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], [])
   (* Is [id] the special variable for recursive notations *)
-  else if ntnvars != [] && id_eq id ldots_var
+  else if ntnvars != [] && Id.equal id ldots_var
   then
     GVar (loc,id), [], [], []
   else
@@ -722,7 +722,7 @@ let intern_applied_reference intern env namedctx lvar args = function
 let interp_reference vars r =
   let (r,_,_,_),_ =
     intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
-      {ids = Idset.empty; unb = false ;
+      {ids = Id.Set.empty; unb = false ;
        tmp_scope = None; scopes = []; impls = empty_internalization_env} []
       (vars,[]) [] r
   in r
@@ -912,7 +912,7 @@ let sort_fields mode loc l completer =
 	  let ind = record.Recordops.s_CONST in
 	  try (* insertion of Constextern.reference_global *)
 	    (record.Recordops.s_EXPECTEDPARAM,
-	     Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef ind)),
+	     Qualid (loc, shortest_qualid_of_global Id.Set.empty (ConstructRef ind)),
 	     build_patt record.Recordops.s_PROJ record.Recordops.s_PROJKIND 1 (0,[]))
 	  with Not_found -> anomaly "Environment corruption for records."
 	  in
@@ -987,7 +987,7 @@ let message_redundant_alias (id1,id2) =
 
 let rec subst_pat_iterator y t p = match p with
   | RCPatAtom (_,id) ->
-    begin match id with Some x when id_eq x y -> t | _ -> p end
+    begin match id with Some x when Id.equal x y -> t | _ -> p end
   | RCPatCstr (loc,id,l1,l2) ->
      RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
 	       List.map (subst_pat_iterator y t) l2)
@@ -1093,8 +1093,8 @@ let drop_notations_pattern looked_for =
 	  in_pat {env with scopes=subscopes@env.scopes;
 	    tmp_scope = scopt} a
 	with Not_found ->
-	  if id_eq id ldots_var then RCPatAtom (loc,Some id) else
-	    anomaly ("Unbound pattern notation variable: "^(string_of_id id))
+	  if Id.equal id ldots_var then RCPatAtom (loc,Some id) else
+	    anomaly ("Unbound pattern notation variable: "^(Id.to_string id))
       end
     | NRef g ->
       looked_for g;
@@ -1209,7 +1209,7 @@ let check_projection isproj nargs r =
 	  user_err_loc (loc,"",str "Projection has not the right number of explicit parameters.");
       with Not_found ->
 	user_err_loc
-	(loc,"",pr_global_env Idset.empty ref ++ str " is not a registered projection."))
+	(loc,"",pr_global_env Id.Set.empty ref ++ str " is not a registered projection."))
   | _, Some _ -> user_err_loc (loc_of_glob_constr r, "", str "Not a projection.")
   | _, None -> ()
 
@@ -1222,7 +1222,7 @@ let set_hole_implicit i b = function
   | _ -> anomaly "Only refs have implicits"
 
 let exists_implicit_name id =
-  List.exists (fun imp -> is_status_implicit imp && id_eq id (name_of_implicit imp))
+  List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp))
 
 let extract_explicit_arg imps args =
   let rec aux = function
@@ -1403,19 +1403,19 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	end
     | CCases (loc, sty, rtnpo, tms, eqns) ->
       let as_in_vars = List.fold_left (fun acc (_,(na,inb)) ->
-	Option.fold_left (fun x tt -> List.fold_right Idset.add (ids_of_cases_indtype tt) x)
-	  (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Idset.add y' x |_ -> x) acc na)
-	  inb) Idset.empty tms in
+	Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x)
+	  (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na)
+	  inb) Id.Set.empty tms in
       (* as, in & return vars *)
       let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
       let tms,ex_ids,match_from_in = List.fold_right
 	(fun citm (inds,ex_ids,matchs) ->
 	  let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in
-	  (tm,ind)::inds, Option.fold_right Idset.add extra_id ex_ids, List.rev_append match_td matchs)
-	    tms ([],Idset.empty,[]) in
-      let env' = Idset.fold
+	  (tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
+	    tms ([],Id.Set.empty,[]) in
+      let env' = Id.Set.fold
 	(fun var bli -> push_name_env lvar (Variable,[],[],[]) bli (Loc.ghost,Name var))
-	(Idset.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
+	(Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
       (* PatVars before a real pattern do not need to be matched *)
       let stripped_match_from_in = let rec aux = function
 	|[] -> []
@@ -1438,7 +1438,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
 	(* "in" is None so no match to add *)
-        let ((b',(na',_)),_,_) = intern_case_item env' Idset.empty (b,(na,None)) in
+        let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,(na,None)) in
         let p' = Option.map (fun u ->
 	  let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
 	    (Loc.ghost,na') in
@@ -1447,7 +1447,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
                    intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
       let env' = reset_tmp_scope env in
-      let ((c',(na',_)),_,_) = intern_case_item env' Idset.empty (c,(na,None)) in (* no "in" no match to ad too *)
+      let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,(na,None)) in (* no "in" no match to ad too *)
       let p' = Option.map (fun p ->
           let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
 	    (Loc.ghost,na') in
@@ -1492,7 +1492,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
     (* Linearity implies the order in ids is irrelevant *)
     check_linearity lhs eqn_ids;
-    let env_ids = List.fold_right Idset.add eqn_ids env.ids in
+    let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
       List.iter message_redundant_alias asubst;
@@ -1504,7 +1504,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let tm' = intern env tm in
     (* the "as" part *)
     let extra_id,na = match tm', na with
-      | GVar (loc,id), None when Idset.mem id env.ids -> Some id,(loc,Name id)
+      | GVar (loc,id), None when Id.Set.mem id env.ids -> Some id,(loc,Name id)
       | GRef (loc, VarRef id), None -> Some id,(loc,Name id)
       | _, None -> None,(Loc.ghost,Anonymous)
       | _, Some (loc,na) -> None,(loc,na) in
@@ -1512,7 +1512,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
     let match_td,typ = match t with
     | Some t ->
 	let tids = ids_of_cases_indtype t in
-	let tids = List.fold_right Idset.add tids Idset.empty in
+	let tids = List.fold_right Id.Set.add tids Id.Set.empty in
 	let with_letin,(ind,l) = intern_ind_pattern globalenv {env with ids = tids; tmp_scope = None} t in
 	let (mib,mip) = Inductive.lookup_mind_specif globalenv ind in
 	let nparams = (List.length (mib.Declarations.mind_params_ctxt)) in
@@ -1544,7 +1544,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	      |_ -> assert false in
 	  let _,args_rel =
 	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
-	  canonize_args args_rel l (Idset.elements forbidden_names_for_gen) [] [] in
+	  canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
 	match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal)
     | None ->
       [], None in
@@ -1618,9 +1618,9 @@ let internalize sigma globalenv env allow_patvar lvar c =
 (**************************************************************************)
 
 let extract_ids env =
-  List.fold_right Idset.add
+  List.fold_right Id.Set.add
     (Termops.ids_of_rel_context (Environ.rel_context env))
-    Idset.empty
+    Id.Set.empty
 
 let scope_of_type_kind = function
   | IsType -> Some Notation.type_scope
@@ -1674,7 +1674,7 @@ let interp_open_constr sigma env c =
 let interp_open_constr_patvar sigma env c =
   let raw = intern_gen (OfType None) sigma env c ~allow_patvar:true in
   let sigma = ref sigma in
-  let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in
+  let evars = ref (Gmap.empty : (Id.t,glob_constr) Gmap.t) in
   let rec patvar_to_evar r = match r with
     | GPatVar (loc,(_,id)) ->
 	( try Gmap.find id !evars
@@ -1724,7 +1724,7 @@ let interp_casted_constr_evars evdref env ?(impls=empty_internalization_env) c t
 let interp_type_evars evdref env ?(impls=empty_internalization_env) c =
   interp_constr_evars_gen evdref env IsType ~impls c
 
-type ltac_sign = identifier list * unbound_ltac_var_map
+type ltac_sign = Id.t list * unbound_ltac_var_map
 
 let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen (if as_type then IsType else OfType None)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 28e7e2985..6cb97fd60 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -41,7 +41,7 @@ open Decl_kinds
    of [env] *)
 
 type var_internalization_type =
-  | Inductive of identifier list (* list of params *)
+  | Inductive of Id.t list (* list of params *)
   | Recursive
   | Method
   | Variable
@@ -50,14 +50,14 @@ type var_internalization_data =
     var_internalization_type *
       (** type of the "free" variable, for coqdoc, e.g. while typing the
 	  constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
-    identifier list *
+    Id.t list *
       (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
           in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
     Impargs.implicit_status list * (** signature of impargs of the variable *)
     Notation_term.scope_name option list (** subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
-type internalization_env = var_internalization_data Idmap.t
+type internalization_env = var_internalization_data Id.Map.t
 
 val empty_internalization_env : internalization_env
 
@@ -65,10 +65,10 @@ val compute_internalization_data : env -> var_internalization_type ->
   types -> Impargs.manual_explicitation list -> var_internalization_data
 
 val compute_internalization_env : env -> var_internalization_type ->
-  identifier list -> types list -> Impargs.manual_explicitation list list ->
+  Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-type ltac_sign = identifier list * unbound_ltac_var_map
+type ltac_sign = Id.t list * unbound_ltac_var_map
 
 type glob_binder = (name * binding_kind * glob_constr option * glob_constr)
 
@@ -83,8 +83,8 @@ val intern_gen : typing_constraint -> evar_map -> env ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
-  Names.identifier list *
-    ((Names.identifier * Names.identifier) list * cases_pattern) list
+  Names.Id.t list *
+    ((Names.Id.t * Names.Id.t) list * cases_pattern) list
 
 val intern_context : bool -> evar_map -> env -> internalization_env -> local_binder list -> internalization_env * glob_binder list
 
@@ -168,19 +168,19 @@ val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
 
-val is_global : identifier -> bool
-val construct_reference : named_context -> identifier -> constr
-val global_reference : identifier -> constr
-val global_reference_in_absolute_module : dir_path -> identifier -> constr
+val is_global : Id.t -> bool
+val construct_reference : named_context -> Id.t -> constr
+val global_reference : Id.t -> constr
+val global_reference_in_absolute_module : dir_path -> Id.t -> constr
 
 (** Interprets a term as the left-hand side of a notation; the boolean
     list is a set and this set is [true] for a variable occurring in
     term position, [false] for a variable occurring in binding
     position; [true;false] if in both kinds of position *)
 val interp_notation_constr : ?impls:internalization_env ->
-  (identifier * notation_var_internalization_type) list ->
-  (identifier * identifier) list -> constr_expr ->
-  (identifier * (subscopes * notation_var_internalization_type)) list *
+  (Id.t * notation_var_internalization_type) list ->
+  (Id.t * Id.t) list -> constr_expr ->
+  (Id.t * (subscopes * notation_var_internalization_type)) list *
   notation_constr
 
 (** Globalization options *)
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 607355873..4b2ca2004 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -21,10 +21,10 @@ open Smartlocate
 
 type message = string
 
-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 global_of_extended_global (Nametab.extended_global_of_path sp)
   with Not_found -> anomaly (locstr^": cannot find "^(string_of_path sp))
 
@@ -63,7 +63,7 @@ let gen_constant_in_modules locstr dirs s =
 (* For tactics/commands requiring vernacular libraries *)
 
 let check_required_library d =
-  let d' = List.map id_of_string d in
+  let d' = List.map Id.of_string d in
   let dir = make_dirpath (List.rev d') in
   let mp = (fst(Lib.current_prefix())) in
   let current_dir = match mp with
@@ -130,14 +130,14 @@ let make_con dir id = Globnames.encode_con dir id
 
 (** Identity *)
 
-let id = make_con datatypes_module (id_of_string "id")
-let type_of_id = make_con datatypes_module (id_of_string "ID")
+let id = make_con datatypes_module (Id.of_string "id")
+let type_of_id = make_con datatypes_module (Id.of_string "ID")
 
 let _ = Termops.set_impossible_default_clause (mkConst id,mkConst type_of_id)
 
 (** Natural numbers *)
-let nat_kn = make_kn datatypes_module (id_of_string "nat")
-let nat_path = Libnames.make_path datatypes_module (id_of_string "nat")
+let nat_kn = make_kn datatypes_module (Id.of_string "nat")
+let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
 
 let glob_nat = IndRef (nat_kn,0)
 
@@ -147,7 +147,7 @@ let glob_O = ConstructRef path_of_O
 let glob_S = ConstructRef path_of_S
 
 (** Booleans *)
-let bool_kn = make_kn datatypes_module (id_of_string "bool")
+let bool_kn = make_kn datatypes_module (Id.of_string "bool")
 
 let glob_bool = IndRef (bool_kn,0)
 
@@ -157,13 +157,13 @@ let glob_true  = ConstructRef path_of_true
 let glob_false  = ConstructRef path_of_false
 
 (** Equality *)
-let eq_kn = make_kn logic_module (id_of_string "eq")
+let eq_kn = make_kn logic_module (Id.of_string "eq")
 let glob_eq = IndRef (eq_kn,0)
 
-let identity_kn = make_kn datatypes_module (id_of_string "identity")
+let identity_kn = make_kn datatypes_module (Id.of_string "identity")
 let glob_identity = IndRef (identity_kn,0)
 
-let jmeq_kn = make_kn jmeq_module (id_of_string "JMeq")
+let jmeq_kn = make_kn jmeq_module (Id.of_string "JMeq")
 let glob_jmeq = IndRef (jmeq_kn,0)
 
 type coq_sigma_data = {
@@ -278,8 +278,8 @@ let build_coq_jmeq_data () =
   congr = Lazy.force coq_jmeq_congr }
 
 let join_jmeq_types eq =
-  mkLambda(Name (id_of_string "A"),Termops.new_Type(),
-  mkLambda(Name (id_of_string "x"),mkRel 1,
+  mkLambda(Name (Id.of_string "A"),Termops.new_Type(),
+  mkLambda(Name (Id.of_string "x"),mkRel 1,
   mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|])))
 
 let build_coq_inversion_jmeq_data () =
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index f87130e57..6ea0d09a4 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -135,7 +135,7 @@ let add_glob_gen loc sp lib_dp ty =
     let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in
     let filepath = Names.string_of_dirpath lib_dp in
     let modpath = Names.string_of_dirpath mod_dp_trunc in
-    let ident = Names.string_of_id id in
+    let ident = Names.Id.to_string id in
       dump_ref loc filepath modpath ident ty
 
 let add_glob loc ref =
@@ -160,7 +160,7 @@ let dump_binding loc id = ()
 let dump_definition (loc, id) sec s =
   let bl,el = interval loc in
   dump_string (Printf.sprintf "%s %d:%d %s %s\n" s bl el
-			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.string_of_id id))
+			(Names.string_of_dirpath (Lib.current_dirpath sec)) (Names.Id.to_string id))
 
 let dump_reference loc modpath ident ty =
   let bl,el = interval loc in
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index a3e67234c..4a0752a3a 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -25,14 +25,14 @@ val continue : unit -> unit
 val add_glob : Loc.t -> Globnames.global_reference -> unit
 val add_glob_kn : Loc.t -> Names.kernel_name -> unit
 
-val dump_definition : Loc.t * Names.identifier -> bool -> string -> unit
+val dump_definition : Loc.t * Names.Id.t -> bool -> string -> unit
 val dump_moddef : Loc.t -> Names.module_path -> string -> unit
 val dump_modref  : Loc.t -> Names.module_path -> string -> unit
 val dump_reference  : Loc.t -> string -> string -> string -> unit
 val dump_libref : Loc.t -> Names.dir_path -> string -> unit
 val dump_notation_location : (int * int) list -> Constrexpr.notation ->
   (Notation.notation_location * Notation_term.scope_name option) -> unit
-val dump_binding : Loc.t -> Names.Idset.elt -> unit
+val dump_binding : Loc.t -> Names.Id.Set.elt -> unit
 val dump_notation :
   Loc.t * (Constrexpr.notation * Notation.notation_location) ->
   Notation_term.scope_name option -> bool -> unit
diff --git a/interp/genarg.mli b/interp/genarg.mli
index b8ed6f374..7bcb5aa11 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -130,21 +130,21 @@ val rawwit_intro_pattern : (intro_pattern_expr located,rlevel) abstract_argument
 val globwit_intro_pattern : (intro_pattern_expr located,glevel) abstract_argument_type
 val wit_intro_pattern : (intro_pattern_expr located,tlevel) abstract_argument_type
 
-val rawwit_ident : (identifier,rlevel) abstract_argument_type
-val globwit_ident : (identifier,glevel) abstract_argument_type
-val wit_ident : (identifier,tlevel) abstract_argument_type
+val rawwit_ident : (Id.t,rlevel) abstract_argument_type
+val globwit_ident : (Id.t,glevel) abstract_argument_type
+val wit_ident : (Id.t,tlevel) abstract_argument_type
 
-val rawwit_pattern_ident : (identifier,rlevel) abstract_argument_type
-val globwit_pattern_ident : (identifier,glevel) abstract_argument_type
-val wit_pattern_ident : (identifier,tlevel) abstract_argument_type
+val rawwit_pattern_ident : (Id.t,rlevel) abstract_argument_type
+val globwit_pattern_ident : (Id.t,glevel) abstract_argument_type
+val wit_pattern_ident : (Id.t,tlevel) abstract_argument_type
 
-val rawwit_ident_gen : bool -> (identifier,rlevel) abstract_argument_type
-val globwit_ident_gen : bool -> (identifier,glevel) abstract_argument_type
-val wit_ident_gen : bool -> (identifier,tlevel) abstract_argument_type
+val rawwit_ident_gen : bool -> (Id.t,rlevel) abstract_argument_type
+val globwit_ident_gen : bool -> (Id.t,glevel) abstract_argument_type
+val wit_ident_gen : bool -> (Id.t,tlevel) abstract_argument_type
 
-val rawwit_var : (identifier located,rlevel) abstract_argument_type
-val globwit_var : (identifier located,glevel) abstract_argument_type
-val wit_var : (identifier,tlevel) abstract_argument_type
+val rawwit_var : (Id.t located,rlevel) abstract_argument_type
+val globwit_var : (Id.t located,glevel) abstract_argument_type
+val wit_var : (Id.t,tlevel) abstract_argument_type
 
 val rawwit_ref : (reference,rlevel) abstract_argument_type
 val globwit_ref : (global_reference located or_var,glevel) abstract_argument_type
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 13c39f60d..480b6a18e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -23,28 +23,28 @@ open Nameops
 open Misctypes
 (*i*)
 
-let generalizable_table = ref Idpred.empty
+let generalizable_table = ref Id.Pred.empty
 
 let _ =
   Summary.declare_summary "generalizable-ident"
     { Summary.freeze_function = (fun () -> !generalizable_table);
       Summary.unfreeze_function = (fun r -> generalizable_table := r);
-      Summary.init_function = (fun () -> generalizable_table := Idpred.empty) }
+      Summary.init_function = (fun () -> generalizable_table := Id.Pred.empty) }
 
 let declare_generalizable_ident table (loc,id) =
-  if not (id_eq id (root_of_id id)) then
+  if not (Id.equal id (root_of_id id)) then
     user_err_loc(loc,"declare_generalizable_ident",
     (pr_id id ++ str
       " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
-  if Idpred.mem id table then
+  if Id.Pred.mem id table then
     user_err_loc(loc,"declare_generalizable_ident",
 		(pr_id id++str" is already declared as a generalizable identifier"))
-  else Idpred.add id table
+  else Id.Pred.add id table
 
 let add_generalizable gen table =
   match gen with
-  | None -> Idpred.empty
-  | Some [] -> Idpred.full
+  | None -> Id.Pred.empty
+  | Some [] -> Id.Pred.full
   | Some l -> List.fold_left (fun table lid -> declare_generalizable_ident table lid)
       table l
 
@@ -54,7 +54,7 @@ let cache_generalizable_type (_,(local,cmd)) =
 let load_generalizable_type _ (_,(local,cmd)) =
   generalizable_table := add_generalizable cmd !generalizable_table
 
-let in_generalizable : bool * identifier Loc.located list option -> obj =
+let in_generalizable : bool * Id.t Loc.located list option -> obj =
   declare_object {(default_object "GENERALIZED-IDENT") with
     load_function = load_generalizable_type;
     cache_function = cache_generalizable_type;
@@ -64,10 +64,10 @@ let in_generalizable : bool * identifier Loc.located list option -> obj =
 let declare_generalizable local gen =
  Lib.add_anonymous_leaf (in_generalizable (local, gen))
 
-let find_generalizable_ident id = Idpred.mem (root_of_id id) !generalizable_table
+let find_generalizable_ident id = Id.Pred.mem (root_of_id id) !generalizable_table
 
 let ids_of_list l =
-  List.fold_right Idset.add l Idset.empty
+  List.fold_right Id.Set.add l Id.Set.empty
 
 let locate_reference qid =
   match Nametab.locate_extended qid with
@@ -82,7 +82,7 @@ let is_global id =
 
 let is_freevar ids env x =
   try
-    if Idset.mem x ids then false
+    if Id.Set.mem x ids then false
     else
       try ignore(Environ.lookup_named x env) ; false
       with _ -> not (is_global x)
@@ -94,7 +94,7 @@ let ungeneralizable loc id =
   user_err_loc (loc, "Generalization", 
 	       str "Unbound and ungeneralizable variable " ++ pr_id id)
 
-let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
+let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
   let found loc id bdvars l =
     if List.mem id l then l
     else if is_freevar bdvars (Global.env ()) id
@@ -105,25 +105,25 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
   in
   let rec aux bdvars l c = match c with
     | CRef (Ident (loc,id)) -> found loc id bdvars l
-    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) ->
-	Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
-    | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+    | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Id.Set.mem id bdvars) ->
+	Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
+    | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
   in aux bound l c
 
 let ids_of_names l =
   List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l
 
-let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
+let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) =
   let rec aux bdvars l c = match c with
       ((LocalRawAssum (n, _, c)) :: tl) ->
 	let bound = ids_of_names n in
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
     | ((LocalRawDef (n, c)) :: tl) ->
 	let bound = match snd n with Anonymous -> [] | Name n -> [n] in
 	let l' = free_vars_of_constr_expr c ~bound:bdvars l in
-	  aux (Idset.union (ids_of_list bound) bdvars) l' tl
+	  aux (Id.Set.union (ids_of_list bound) bdvars) l' tl
 
     | [] -> bdvars, l
   in aux bound l binders
@@ -131,9 +131,9 @@ let free_vars_of_binders ?(bound=Idset.empty) l (binders : local_binder list) =
 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 generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty) =
+let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
   let rec vars bound vs = function
     | GVar (loc,id) ->
 	if is_freevar bound (Global.env ()) id then
@@ -160,7 +160,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty
 	let vs3 = vars bound vs2 b1 in
 	vars bound vs3 b2
     | GRec (loc,fk,idl,bl,tyl,bv) ->
-	let bound' = Array.fold_right Idset.add idl bound in
+	let bound' = Array.fold_right Id.Set.add idl bound in
 	let vars_fix i vs fid =
 	  let vs1,bound1 =
 	    List.fold_left
@@ -182,7 +182,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
   and vars_pattern bound vs (loc,idl,p,c) =
-    let bound' = List.fold_right Idset.add idl bound  in
+    let bound' = List.fold_right Id.Set.add idl bound  in
     vars bound' vs c
 
   and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
@@ -193,7 +193,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty
   in fun rt -> 
     let vars = List.rev (vars bound [] rt) in
       List.iter (fun (id, loc) ->
-	if not (Idset.mem id allowed || find_generalizable_ident id) then 
+	if not (Id.Set.mem id allowed || find_generalizable_ident id) then 
 	  ungeneralizable loc id) vars;
       vars
 
@@ -202,7 +202,7 @@ let rec make_fresh ids env x =
 
 let next_name_away_from na avoid =
   match na with
-  | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
+  | Anonymous -> make_fresh avoid (Global.env ()) (Id.of_string "anon")
   | Name id -> make_fresh avoid (Global.env ()) id
 
 let combine_params avoid fn applied needed =
@@ -211,7 +211,7 @@ let combine_params avoid fn applied needed =
       (function
 	  (t, Some (loc, ExplByName id)) ->
             let is_id (_, (na, _, _)) = match na with
-            | Name id' -> id_eq id id'
+            | Name id' -> Id.equal id id'
             | Anonymous -> false
             in
 	    if not (List.exists is_id needed) then
@@ -255,7 +255,7 @@ let combine_params avoid fn applied needed =
 let combine_params_freevar =
   fun avoid (_, (na, _, _)) ->
     let id' = next_name_away_from na avoid in
-      (CRef (Ident (Loc.ghost, id')), Idset.add id' avoid)
+      (CRef (Ident (Loc.ghost, id')), Id.Set.add id' avoid)
 
 let destClassApp cl =
   match cl with
@@ -282,7 +282,7 @@ let implicit_application env ?(allow_partial=true) f ty =
     match is_class with
     | None -> ty, env
     | Some ((loc, id, par), gr) ->
-	let avoid = Idset.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
+	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
 	  let c = class_info gr in
 	  let (ci, rd) = c.cl_context in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 256f65ba2..2c5ad7408 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -22,35 +22,35 @@ open Libnames
 open Globnames
 open Typeclasses
 
-val declare_generalizable : Vernacexpr.locality_flag -> (identifier located) list option -> unit
+val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
 
-val ids_of_list : identifier list -> Idset.t
+val ids_of_list : Id.t list -> Id.Set.t
 val destClassApp : constr_expr -> Loc.t * reference * constr_expr list
 val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list
 
 (** Fragile, should be used only for construction a set of identifiers to avoid *)
 
-val free_vars_of_constr_expr : constr_expr -> ?bound:Idset.t ->
-  identifier list -> identifier list
+val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t ->
+  Id.t list -> Id.t list
 
 val free_vars_of_binders :
-  ?bound:Idset.t -> Names.identifier list -> local_binder list -> Idset.t * Names.identifier list
+  ?bound:Id.Set.t -> Names.Id.t list -> local_binder list -> Id.Set.t * Names.Id.t list
 
 (** Returns the generalizable free ids in left-to-right
    order with the location of their first occurence *)
 
-val generalizable_vars_of_glob_constr : ?bound:Idset.t -> ?allowed:Idset.t ->
-  glob_constr -> (Names.identifier * Loc.t) list
+val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
+  glob_constr -> (Names.Id.t * Loc.t) list
 
-val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
+val make_fresh : Names.Id.Set.t -> Environ.env -> Id.t -> Id.t
 
 val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits
 
 val combine_params_freevar :
-  Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-  Constrexpr.constr_expr * Names.Idset.t
+  Names.Id.Set.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
+  Constrexpr.constr_expr * Names.Id.Set.t
 
-val implicit_application : Idset.t -> ?allow_partial:bool ->
-  (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-    Constrexpr.constr_expr * Names.Idset.t) ->
-  constr_expr -> constr_expr * Idset.t
+val implicit_application : Id.Set.t -> ?allow_partial:bool ->
+  (Names.Id.Set.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
+    Constrexpr.constr_expr * Names.Id.Set.t) ->
+  constr_expr -> constr_expr * Id.Set.t
diff --git a/interp/notation.ml b/interp/notation.ml
index 8a01c5985..d5aa59788 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -643,15 +643,15 @@ let declare_ref_arguments_scope ref =
 
 type symbol =
   | Terminal of string
-  | NonTerminal of identifier
-  | SProdList of identifier * symbol list
+  | NonTerminal of Id.t
+  | SProdList of Id.t * symbol list
   | Break of int
 
 let rec symbol_eq s1 s2 = match s1, s2 with
 | Terminal s1, Terminal s2 -> String.equal s1 s2
-| NonTerminal id1, NonTerminal id2 -> id_eq id1 id2
+| NonTerminal id1, NonTerminal id2 -> Id.equal id1 id2
 | SProdList (id1, l1), SProdList (id2, l2) ->
-  id_eq id1 id2 && List.equal symbol_eq l1 l2
+  Id.equal id1 id2 && List.equal symbol_eq l1 l2
 | Break i1, Break i2 -> Int.equal i1 i2
 | _ -> false
 
@@ -677,7 +677,7 @@ let decompose_notation_key s =
     in
     let tok =
       match String.sub s n (pos-n) with
-      | "_" -> NonTerminal (id_of_string "_")
+      | "_" -> NonTerminal (Id.of_string "_")
       | s -> Terminal (String.drop_simple_quotes s) in
     decomp_ntn (tok::dirs) (pos+1)
   in
@@ -695,7 +695,7 @@ let classes_of_scope sc =
 
 let pr_scope_class = function
   | ScopeSort -> str "Sort"
-  | ScopeRef t -> pr_global_env Idset.empty t
+  | ScopeRef t -> pr_global_env Id.Set.empty t
 
 let pr_scope_classes sc =
   let l = classes_of_scope sc in
diff --git a/interp/notation.mli b/interp/notation.mli
index 5c8dbb40b..c3106f5d3 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -169,8 +169,8 @@ val compute_scope_of_global : global_reference -> scope_name option
 
 type symbol =
   | Terminal of string
-  | NonTerminal of identifier
-  | SProdList of identifier * symbol list
+  | NonTerminal of Id.t
+  | SProdList of Id.t * symbol list
   | Break of int
 
 val symbol_eq : symbol -> symbol -> bool
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index c0289fbad..a7e591383 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -50,7 +50,7 @@ let rec subst_glob_vars l = function
       GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
   | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
 
-let ldots_var = id_of_string ".."
+let ldots_var = Id.of_string ".."
 
 let glob_constr_of_notation_constr_with_binders loc g f e = function
   | NVar id -> GVar (loc,id)
@@ -122,7 +122,7 @@ let add_name r = function Anonymous -> () | Name id -> add_id r id
 let split_at_recursive_part c =
   let sub = ref None in
   let rec aux = function
-  | GApp (loc0,GVar(loc,v),c::l) when id_eq v ldots_var ->
+  | GApp (loc0,GVar(loc,v),c::l) when Id.equal v ldots_var ->
       begin match !sub with
       | None ->
         let () = sub := Some c in
@@ -140,14 +140,14 @@ let split_at_recursive_part c =
   | None -> (* No recursive pattern found *) raise Not_found
   | Some c ->
   match outer_iterator with
-  | GVar (_,v) when id_eq v ldots_var -> (* Not enough context *) raise Not_found
+  | GVar (_,v) when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
   | _ -> outer_iterator, c
 
 let on_true_do b f c = if b then (f c; b) else b
 
 let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GRef (_,r1), GRef (_,r2) -> eq_gr r1 r2
-  | GVar (_,v1), GVar (_,v2) -> on_true_do (id_eq v1 v2) add (Name v1)
+  | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
   | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
   | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
     when name_eq na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
@@ -181,18 +181,18 @@ let compare_recursive_parts found f (iterator,subc) =
   let diff = ref None in
   let terminator = ref None in
   let rec aux c1 c2 = match c1,c2 with
-  | GVar(_,v), term when id_eq v ldots_var ->
+  | GVar(_,v), term when Id.equal v ldots_var ->
       (* We found the pattern *)
       assert (match !terminator with None -> true | Some _ -> false);
       terminator := Some term;
       true
-  | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when id_eq v ldots_var ->
+  | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when Id.equal v ldots_var ->
       (* We found the pattern, but there are extra arguments *)
       (* (this allows e.g. alternative (recursive) notation of application) *)
       assert (match !terminator with None -> true | Some _ -> false);
       terminator := Some term;
       List.for_all2eq aux l1 l2
-  | GVar (_,x), GVar (_,y) when not (id_eq x y) ->
+  | GVar (_,x), GVar (_,y) when not (Id.equal x y) ->
       (* We found the position where it differs *)
       let lassoc = match !terminator with None -> false | Some _ -> true in
       let x,y = if lassoc then y,x else x,y in
@@ -249,7 +249,7 @@ let notation_constr_and_vars_of_glob_constr a =
     with Not_found ->
     found := keepfound;
     match c with
-    | GApp (_,GVar (loc,f),[c]) when id_eq f ldots_var ->
+    | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var ->
 	(* Fall on the second part of the recursive pattern w/o having
 	   found the first part *)
 	user_err_loc (loc,"",
@@ -300,7 +300,7 @@ let notation_constr_and_vars_of_glob_constr a =
 
 let rec list_rev_mem_assoc x = function
   | [] -> false
-  | (_,x')::l -> id_eq x x' || list_rev_mem_assoc x l
+  | (_,x')::l -> Id.equal x x' || list_rev_mem_assoc x l
 
 let check_variables vars recvars (found,foundrec,foundrecbinding) =
   let useless_vars = List.map snd recvars in
@@ -316,9 +316,9 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
       if List.mem_assoc x foundrec or List.mem_assoc x foundrecbinding
 	or list_rev_mem_assoc x foundrec or list_rev_mem_assoc x foundrecbinding
       then
-	error ((string_of_id x)^" should not be bound in a recursive pattern of the right-hand side.")
+	error ((Id.to_string x)^" should not be bound in a recursive pattern of the right-hand side.")
       else
-	error ((string_of_id x)^" is unbound in the right-hand side.") in
+	error ((Id.to_string x)^" is unbound in the right-hand side.") in
   let check_pair s x y where =
     if not (List.mem (x,y) where) then
       errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++
@@ -493,10 +493,10 @@ let abstract_return_type_context_notation_constr =
 exception No_match
 
 let rec alpha_var id1 id2 = function
-  | (i1,i2)::_ when id_eq i1 id1 -> id_eq i2 id2
-  | (i1,i2)::_ when id_eq i2 id2 -> id_eq i1 id1
+  | (i1,i2)::_ when Id.equal i1 id1 -> Id.equal i2 id2
+  | (i1,i2)::_ when Id.equal i2 id2 -> Id.equal i1 id1
   | _::idl -> alpha_var id1 id2 idl
-  | [] -> id_eq id1 id2
+  | [] -> Id.equal id1 id2
 
 let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v =
   try
@@ -636,7 +636,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   (* Matching compositionally *)
   | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma
   | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma
-  | GPatVar (_,(_,n1)), NPatVar n2 when id_eq n1 n2 -> sigma
+  | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma
   | GApp (loc,f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index b2df95901..35c9a8e1c 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -17,11 +17,11 @@ open Glob_term
     bound by the notation; also interpret recursive patterns           *)
 
 val notation_constr_of_glob_constr :
-  (identifier * notation_var_internalization_type) list ->
-  (identifier * identifier) list -> glob_constr -> notation_constr
+  (Id.t * notation_var_internalization_type) list ->
+  (Id.t * Id.t) list -> glob_constr -> notation_constr
 
 (** Name of the special identifier used to encode recursive notations  *)
-val ldots_var : identifier
+val ldots_var : Id.t
 
 (** Equality of [glob_constr] (warning: only partially implemented) *)
 (** FIXME: nothing to do here *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 3a865cb7d..30953007e 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -22,7 +22,7 @@ type key =
   | RefKey of global_reference
   | Oth
 
-let reserve_table = ref Idmap.empty
+let reserve_table = ref Id.Map.empty
 let reserve_revtable = ref Gmapl.empty
 
 let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
@@ -34,17 +34,17 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
 
 let cache_reserved_type (_,(id,t)) =
   let key = fst (notation_constr_key t) in
-  reserve_table := Idmap.add id t !reserve_table;
+  reserve_table := Id.Map.add id t !reserve_table;
   reserve_revtable := Gmapl.add key (t,id) !reserve_revtable
 
-let in_reserved : identifier * notation_constr -> obj =
+let in_reserved : Id.t * notation_constr -> obj =
   declare_object {(default_object "RESERVED-TYPE") with
     cache_function = cache_reserved_type }
 
 let freeze_reserved () = (!reserve_table,!reserve_revtable)
 let unfreeze_reserved (r,rr) = reserve_table := r; reserve_revtable := rr
 let init_reserved () =
-  reserve_table := Idmap.empty; reserve_revtable := Gmapl.empty
+  reserve_table := Id.Map.empty; reserve_revtable := Gmapl.empty
 
 let _ =
   Summary.declare_summary "reserved-type"
@@ -53,12 +53,12 @@ let _ =
       Summary.init_function = init_reserved }
 
 let declare_reserved_type_binding (loc,id) t =
-  if not (id_eq id (root_of_id id)) then
+  if not (Id.equal id (root_of_id id)) then
     user_err_loc(loc,"declare_reserved_type",
     (pr_id id ++ str
       " is not reservable: it must have no trailing digits, quote, or _"));
   begin try
-    let _ = Idmap.find id !reserve_table in
+    let _ = Id.Map.find id !reserve_table in
     user_err_loc(loc,"declare_reserved_type",
     (pr_id id++str" is already bound to a type"))
   with Not_found -> () end;
@@ -67,7 +67,7 @@ let declare_reserved_type_binding (loc,id) t =
 let declare_reserved_type idl t =
   List.iter (fun id -> declare_reserved_type_binding id t) (List.rev idl)
 
-let find_reserved_type id = Idmap.find (root_of_id id) !reserve_table
+let find_reserved_type id = Id.Map.find (root_of_id id) !reserve_table
 
 let constr_key c =
   try RefKey (canonical_gr (global_of_constr (fst (Term.decompose_app c))))
diff --git a/interp/reserve.mli b/interp/reserve.mli
index e6c1946a5..305480840 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -12,6 +12,6 @@ open Names
 open Glob_term
 open Notation_term
 
-val declare_reserved_type : identifier located list -> notation_constr -> unit
-val find_reserved_type : identifier -> notation_constr
+val declare_reserved_type : Id.t located list -> notation_constr -> unit
+val find_reserved_type : Id.t -> notation_constr
 val anonymize_if_reserved : name -> glob_constr -> glob_constr
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index cabd207e2..254805f6a 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -41,8 +41,8 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 
 let is_alias_of_already_visible_name sp = function
   | _,NRef ref ->
-      let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in
-      dir_path_eq dir empty_dirpath && id_eq id (basename sp)
+      let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
+      dir_path_eq dir empty_dirpath && Id.equal id (basename sp)
   | _ ->
       false
 
@@ -76,7 +76,7 @@ let in_syntax_constant
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
-type syndef_interpretation = (identifier * subscopes) list * notation_constr
+type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 
 (* Coercions to the general format of notation that also supports
    variables bound to list of expressions *)
@@ -86,8 +86,8 @@ let out_pat (ids,ac) = (List.map (fun (id,(sc,typ)) -> (id,sc)) ids,ac)
 let declare_syntactic_definition local id onlyparse pat =
   let _ = add_leaf id (in_syntax_constant (local,in_pat pat,onlyparse)) in ()
 
-let pr_global r = pr_global_env Idset.empty r
-let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Idset.empty kn)
+let pr_global r = pr_global_env Id.Set.empty r
+let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn)
 
 let allow_compat_notations = ref true
 let verbose_compat_notations = ref false
@@ -101,7 +101,7 @@ let verbose_compat kn def = function
       if !verbose_compat_notations then msg_warning else errorlabstrm ""
     in
     let pp_def = match def with
-      | [], NRef r -> str " is " ++ pr_global_env Idset.empty r
+      | [], NRef r -> str " is " ++ pr_global_env Id.Set.empty r
       | _ -> str " is a compatibility notation"
     in
     let since = str (" since Coq > " ^ Flags.pr_version v ^ ".") in
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 26e98f67c..f3c4a61e6 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -14,9 +14,9 @@ open Libnames
 
 (** Syntactic definitions. *)
 
-type syndef_interpretation = (identifier * subscopes) list * notation_constr
+type syndef_interpretation = (Id.t * subscopes) list * notation_constr
 
-val declare_syntactic_definition : bool -> identifier ->
+val declare_syntactic_definition : bool -> Id.t ->
   Flags.compat_version option -> syndef_interpretation -> unit
 
 val search_syntactic_definition : kernel_name -> syndef_interpretation
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 046904cf5..7f6f5672b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -79,8 +79,8 @@ let rec cases_pattern_fold_names f a = function
 let ids_of_pattern_list =
   List.fold_left
     (Loc.located_fold_left
-      (List.fold_left (cases_pattern_fold_names Idset.add)))
-    Idset.empty
+      (List.fold_left (cases_pattern_fold_names Id.Set.add)))
+    Id.Set.empty
 
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
@@ -123,7 +123,7 @@ let fold_constr_expr_with_binders g f n acc = function
       let acc = List.fold_left (f n) acc (List.map fst al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
-	f (Idset.fold g ids n) acc rhs) bl acc
+	f (Id.Set.fold g ids n) acc rhs) bl acc
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let n' = List.fold_right (Loc.down_located (name_fold g)) nal n in
       f (Option.fold_right (Loc.down_located (name_fold g)) ona n') (f n acc b) c
@@ -141,11 +141,11 @@ let fold_constr_expr_with_binders g f n acc = function
 
 let free_vars_of_constr_expr c =
   let rec aux bdvars l = function
-  | CRef (Ident (_,id)) -> if List.mem id bdvars then l else Idset.add id l
+  | CRef (Ident (_,id)) -> if List.mem id bdvars then l else Id.Set.add id l
   | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
-  in aux [] Idset.empty c
+  in aux [] Id.Set.empty c
 
-let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
+let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
 
 (* Interpret the index of a recursion order annotation *)
 
@@ -161,7 +161,7 @@ let split_at_annot bl na =
       let rec aux acc = function
 	| LocalRawAssum (bls, k, t) as x :: rest ->
             let test (_, na) = match na with
-            | Name id' -> id_eq id id'
+            | Name id' -> Id.equal id id'
             | Anonymous -> false
             in
 	    let l, r = List.split_when test bls in
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index a4228c762..6cc3615f0 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -25,26 +25,26 @@ val oldfashion_patterns : bool ref
 (** Utilities on constr_expr                                           *)
 
 val replace_vars_constr_expr :
-  (identifier * identifier) list -> constr_expr -> constr_expr
+  (Id.t * Id.t) list -> constr_expr -> constr_expr
 
-val free_vars_of_constr_expr : constr_expr -> Idset.t
-val occur_var_constr_expr : identifier -> constr_expr -> bool
+val free_vars_of_constr_expr : constr_expr -> Id.Set.t
+val occur_var_constr_expr : Id.t -> constr_expr -> bool
 
 (** Specific function for interning "in indtype" syntax of "match" *)
-val ids_of_cases_indtype : cases_pattern_expr -> identifier list
+val ids_of_cases_indtype : cases_pattern_expr -> Id.t list
 
-val split_at_annot : local_binder list -> identifier located option -> local_binder list * local_binder list
+val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list
 
 (** Used in typeclasses *)
 
-val fold_constr_expr_with_binders : (identifier -> 'a -> 'a) ->
+val fold_constr_expr_with_binders : (Id.t -> 'a -> 'a) ->
    ('a -> 'b -> constr_expr -> 'b) -> 'a -> 'b -> constr_expr -> 'b
 
 (** Used in correctness and interface; absence of var capture not guaranteed 
    in pattern-matching clauses and in binders of the form [x,y:T(x)] *)
 
 val map_constr_expr_with_binders :
-  (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
+  (Id.t -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
       'a -> constr_expr -> constr_expr
 
 val ntn_loc :