[api] Deprecate all legacy uses of Name.Id in core.

This is a first step towards some of the solutions proposed in #6008.

31 files changed, 90 insertions, 90 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index eabfb7b39..38efcca05 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -306,7 +306,7 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) =
   in
   let extract_if_neq id = function
     | Anonymous -> None
-    | Name id' when id_ord id id' = 0 -> None
+    | Name id' when Id.compare id id' = 0 -> None
     | Name id' -> Some id'
   in
   let na = RelDecl.get_name decl in
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index ee0fae3d4..2f85bc733 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -223,7 +223,7 @@ val push_rel_decl_to_named_context :
   evar_map -> rel_declaration -> ext_named_context -> ext_named_context
 
 val push_rel_context_to_named_context : Environ.env -> evar_map -> types ->
-  named_context_val * types * constr list * csubst * (identifier*constr) list
+  named_context_val * types * constr list * csubst * (Id.t*constr) list
 
 val generalize_evar_over_rels : evar_map -> existential -> types * constr list
 
diff --git a/engine/evd.ml b/engine/evd.ml
index a668826a7..86ab2263f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -370,17 +370,17 @@ val key : Id.t -> t -> Evar.t
 end =
 struct
 
-type t = Id.t EvMap.t * existential_key Idmap.t
+type t = Id.t EvMap.t * existential_key Id.Map.t
 
-let empty = (EvMap.empty, Idmap.empty)
+let empty = (EvMap.empty, Id.Map.empty)
 
 let add_name_newly_undefined id evk evi (evtoid, idtoev as names) =
   match id with
   | None -> names
   | Some id ->
-    if Idmap.mem id idtoev then
+    if Id.Map.mem id idtoev then
       user_err  (str "Already an existential evar of name " ++ pr_id id);
-    (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+    (EvMap.add evk id evtoid, Id.Map.add id evk idtoev)
 
 let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
   if EvMap.mem evk evtoid then
@@ -392,15 +392,15 @@ let remove_name_defined evk (evtoid, idtoev as names) =
   let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
   match id with
   | None -> names
-  | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+  | Some id -> (EvMap.remove evk evtoid, Id.Map.remove id idtoev)
 
 let rename evk id (evtoid, idtoev) =
   let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in
   match id' with
-  | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+  | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev)
   | Some id' ->
-    if Idmap.mem id idtoev then anomaly (str "Evar name already in use.");
-    (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
+    if Id.Map.mem id idtoev then anomaly (str "Evar name already in use.");
+    (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev))
 
 let reassign_name_defined evk evk' (evtoid, idtoev as names) =
   let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
@@ -408,13 +408,13 @@ let reassign_name_defined evk evk' (evtoid, idtoev as names) =
   | None -> names (** evk' must not be defined *)
   | Some id ->
     (EvMap.add evk' id (EvMap.remove evk evtoid),
-    Idmap.add id evk' (Idmap.remove id idtoev))
+    Id.Map.add id evk' (Id.Map.remove id idtoev))
 
 let ident evk (evtoid, _) =
   try Some (EvMap.find evk evtoid) with Not_found -> None
 
 let key id (_, idtoev) =
-  Idmap.find id idtoev
+  Id.Map.find id idtoev
 
 end
 
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bb4227b4a..bd6aa0911 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1192,7 +1192,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
   | PSort s -> GSort s
 
 let extern_constr_pattern env sigma pat =
-  extern true (None,[]) Id.Set.empty (glob_of_pat Idset.empty env sigma pat)
+  extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat)
 
 let extern_rel_context where env sigma sign =
   let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
diff --git a/interp/declare.ml b/interp/declare.ml
index 7fcb38296..bd8f3db50 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -464,7 +464,7 @@ let cache_universes (p, l) =
   let glob = Global.global_universe_names () in
   let glob', ctx =
     List.fold_left (fun ((idl,lid),ctx) (id, lev) ->
-        ((Idmap.add id (p, lev) idl,
+        ((Id.Map.add id (p, lev) idl,
           Univ.LMap.add lev id lid),
          Univ.ContextSet.add_universe lev ctx))
       (glob, Univ.ContextSet.empty) l
@@ -525,7 +525,7 @@ let do_constraint poly l =
                      (str "Cannot declare constraints on anonymous universes")
     | GType (Some (loc, Name id)) ->
        let names, _ = Global.global_universe_names () in
-       try loc, Idmap.find id names
+       try loc, Id.Map.find id names
        with Not_found ->
          user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
   in
diff --git a/kernel/names.mli b/kernel/names.mli
index d111dd3c0..d97fd2b3a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -546,28 +546,28 @@ val eq_ind_chk : inductive -> inductive -> bool
 (** {5 Identifiers} *)
 
 type identifier = Id.t
-(** @deprecated Alias for [Id.t] *)
+[@@ocaml.deprecated "Alias for [Id.t]"]
 
-val string_of_id : identifier -> string
-(** @deprecated Same as [Id.to_string]. *)
+val string_of_id : Id.t -> string
+[@@ocaml.deprecated "Same as [Id.to_string]."]
 
-val id_of_string : string -> identifier
-(** @deprecated Same as [Id.of_string]. *)
+val id_of_string : string -> Id.t
+[@@ocaml.deprecated "Same as [Id.of_string]."]
 
-val id_ord : identifier -> identifier -> int
-(** @deprecated Same as [Id.compare]. *)
+val id_ord : Id.t -> Id.t -> int
+[@@ocaml.deprecated "Same as [Id.compare]."]
 
-val id_eq : identifier -> identifier -> bool
-(** @deprecated Same as [Id.equal]. *)
+val id_eq : Id.t -> Id.t -> bool
+[@@ocaml.deprecated "Same as [Id.equal]."]
 
-module Idset  : Set.S with type elt = identifier and type t = Id.Set.t
-(** @deprecated Same as [Id.Set]. *)
+module Idset  : Set.S with type elt = Id.t and type t = Id.Set.t
+[@@ocaml.deprecated "Same as [Id.Set]."]
 
-module Idpred : Predicate.S with type elt = identifier and type t = Id.Pred.t
-(** @deprecated Same as [Id.Pred]. *)
+module Idpred : Predicate.S with type elt = Id.t and type t = Id.Pred.t
+[@@ocaml.deprecated "Same as [Id.Pred]."]
 
 module Idmap : module type of Id.Map
-(** @deprecated Same as [Id.Map]. *)
+[@@ocaml.deprecated "Same as [Id.Map]."]
 
 (** {5 Directory paths} *)
 
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index e08d913bc..6e9991ac5 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -59,7 +59,7 @@ type gname =
   | Gnormtbl of label option * int
   | Ginternal of string
   | Grel of int
-  | Gnamed of identifier
+  | Gnamed of Id.t
 
 let eq_gname gn1 gn2 =
   match gn1, gn2 with
@@ -266,7 +266,7 @@ type primitive =
   | Mk_fix of rec_pos * int 
   | Mk_cofix of int
   | Mk_rel of int
-  | Mk_var of identifier
+  | Mk_var of Id.t
   | Mk_proj
   | Is_accu
   | Is_int
@@ -625,7 +625,7 @@ let decompose_MLlam c =
 
 (*s Global declaration *)
 type global =
-(*  | Gtblname of gname * identifier array *)
+(*  | Gtblname of gname * Id.t array *)
   | Gtblnorm of gname * lname array * mllambda array 
   | Gtblfixtype of gname * lname array * mllambda array
   | Glet of gname * mllambda
@@ -732,7 +732,7 @@ type env =
       env_bound : int; (* length of env_rel *)
       (* free variables *)
       env_urel : (int * mllambda) list ref; (* list of unbound rel *)
-      env_named : (identifier * mllambda) list ref;
+      env_named : (Id.t * mllambda) list ref;
       env_univ : lname option}
 
 let empty_env univ () =
@@ -1955,8 +1955,8 @@ let is_code_loaded ~interactive name =
       if is_loaded_native_file s then true
       else (name := NotLinked; false)
 
-let param_name = Name (id_of_string "params")
-let arg_name = Name (id_of_string "arg")
+let param_name = Name (Id.of_string "params")
+let arg_name = Name (Id.of_string "arg")
 
 let compile_mind prefix ~interactive mb mind stack =
   let u = Declareops.inductive_polymorphic_context mb in
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 2353470f0..73f18f7a7 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -21,7 +21,7 @@ type uint =
 
 and lambda =
   | Lrel          of name * int 
-  | Lvar          of identifier
+  | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
   | Levar         of existential * lambda (* type *)
   | Lprod         of lambda * lambda 
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 7463a30fe..1c9996d89 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -52,7 +52,7 @@ type atom =
   | Aconstant of pconstant
   | Aind of pinductive
   | Asort of sorts
-  | Avar of identifier
+  | Avar of Id.t
   | Acase of annot_sw * accumulator * t * (t -> t)
   | Afix of t array * t array * rec_pos * int
             (* types, bodies, rec_pos, pos *)
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 49b1e122d..0e2db8486 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -44,7 +44,7 @@ type atom =
   | Aconstant of pconstant
   | Aind of pinductive
   | Asort of sorts
-  | Avar of identifier
+  | Avar of Id.t
   | Acase of annot_sw * accumulator * t * (t -> t) 
   | Afix of t array * t array * rec_pos * int 
   | Acofix of t array * t array * int * t
@@ -62,7 +62,7 @@ val mk_rels_accu : int -> int -> t array
 val mk_constant_accu : constant -> Univ.Level.t array -> t
 val mk_ind_accu : inductive -> Univ.Level.t array -> t
 val mk_sort_accu : sorts -> Univ.Level.t array -> t
-val mk_var_accu : identifier -> t
+val mk_var_accu : Id.t -> t
 val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t)
 val mk_prod_accu : name -> t -> t -> t
 val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f93b24b3e..e28c8e826 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -385,10 +385,10 @@ let build_constant_declaration kn env result =
     let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
     if not (Id.Set.subset inferred_set declared_set) then
-      let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
+      let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in
       let n = List.length l in
-      let declared_vars = Pp.pr_sequence Id.print (Idset.elements declared_set) in
-      let inferred_vars = Pp.pr_sequence Id.print (Idset.elements inferred_set) in
+      let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in
+      let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in
       let missing_vars  = Pp.pr_sequence Id.print (List.rev l) in
       user_err Pp.(prlist str
          ["The following section "; (String.plural n "variable"); " ";
@@ -414,7 +414,7 @@ let build_constant_declaration kn env result =
            we must look at the body NOW, if any *)
         let ids_typ = global_vars_set env typ in
         let ids_def = match def with
-        | Undef _ -> Idset.empty
+        | Undef _ -> Id.Set.empty
         | Def cs -> global_vars_set env (Mod_subst.force_constr cs)
         | OpaqueDef lc ->
             let vars =
@@ -425,7 +425,7 @@ let build_constant_declaration kn env result =
             if !Flags.record_aux_file then record_aux env ids_typ vars;
             vars
         in
-        keep_hyps env (Idset.union ids_typ ids_def), def
+        keep_hyps env (Id.Set.union ids_typ ids_def), def
     | None ->
         if !Flags.record_aux_file then
           record_aux env Id.Set.empty Id.Set.empty;
@@ -438,14 +438,14 @@ let build_constant_declaration kn env result =
         | Def cs as x ->
             let ids_typ = global_vars_set env typ in
             let ids_def = global_vars_set env (Mod_subst.force_constr cs) in
-            let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+            let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
             check declared inferred;
             x
         | OpaqueDef lc -> (* In this case we can postpone the check *)
             OpaqueDef (Opaqueproof.iter_direct_opaque (fun c ->
               let ids_typ = global_vars_set env typ in
               let ids_def = global_vars_set env c in
-              let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+              let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in
               check declared inferred) lc) in
   let univs = result.cook_universes in
   let tps = 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index bbaf569d3..9813fc566 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -44,7 +44,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of identifier * 'constr
+  | ReferenceVariables of Id.t * 'constr
   | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 1b2ccf8f8..95a963da2 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -45,7 +45,7 @@ type ('constr, 'types) ptype_error =
   | UnboundVar of variable
   | NotAType of ('constr, 'types) punsafe_judgment
   | BadAssumption of ('constr, 'types) punsafe_judgment
-  | ReferenceVariables of identifier * 'constr
+  | ReferenceVariables of Id.t * 'constr
   | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment
       * (sorts_family * sorts_family * arity_error) option
   | CaseNotInductive of ('constr, 'types) punsafe_judgment
@@ -74,7 +74,7 @@ val error_not_type : env -> unsafe_judgment -> 'a
 
 val error_assumption : env -> unsafe_judgment -> 'a
 
-val error_reference_variables : env -> identifier -> constr -> 'a
+val error_reference_variables : env -> Id.t -> constr -> 'a
 
 val error_elim_arity :
   env -> pinductive -> sorts_family list -> constr -> unsafe_judgment ->
diff --git a/library/global.ml b/library/global.ml
index 963c97741..28b9e66f8 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -233,11 +233,11 @@ let universes_of_global gr =
 
 (** Global universe names *)
 type universe_names = 
-  (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
+  (polymorphic * Univ.universe_level) Id.Map.t * Id.t Univ.LMap.t
 
 let global_universes =
   Summary.ref ~name:"Global universe names"
-  ((Idmap.empty, Univ.LMap.empty) : universe_names)
+  ((Id.Map.empty, Univ.LMap.empty) : universe_names)
 
 let global_universe_names () = !global_universes
 let set_global_universe_names s = global_universes := s
diff --git a/library/global.mli b/library/global.mli
index c777691d1..15bf58f82 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -104,7 +104,7 @@ val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AU
 
 (** Global universe name <-> level mapping *)
 type universe_names = 
-  (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t
+  (Decl_kinds.polymorphic * Univ.universe_level) Id.Map.t * Id.t Univ.LMap.t
 
 val global_universe_names : unit -> universe_names
 val set_global_universe_names : universe_names -> unit
diff --git a/library/globnames.ml b/library/globnames.ml
index dc9541a0d..5c75994dd 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -84,7 +84,7 @@ let is_global c t =
   | ConstRef c, Const (c', _) -> eq_constant c c'
   | IndRef i, Ind (i', _) -> eq_ind i i'
   | ConstructRef i, Construct (i', _) -> eq_constructor i i'
-  | VarRef id, Var id' -> id_eq id id'
+  | VarRef id, Var id' -> Id.equal id id'
   | _ -> false
 
 let printable_constr_of_global = function
diff --git a/library/lib.ml b/library/lib.ml
index 5418003eb..e95bb47f2 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -505,7 +505,7 @@ let variable_section_segment_of_reference = function
 let section_instance = function
   | VarRef id ->
      let eq = function
-       | Variable (id',_,_,_) -> Names.id_eq id id'
+       | Variable (id',_,_,_) -> Names.Id.equal id id'
        | Context _ -> false
      in
      if List.exists eq (pi1 (List.hd !sectab))
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 9128d4042..ddef1cee9 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -213,7 +213,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
   let open EConstr in
   let convref ref c = 
     match ref, EConstr.kind sigma c with
-    | VarRef id, Var id' -> Names.id_eq id id'
+    | VarRef id, Var id' -> Names.Id.equal id id'
     | ConstRef c, Const (c',_) -> Names.eq_constant c c'
     | IndRef i, Ind (i', _) -> Names.eq_ind i i'
     | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 7f81d1aa3..e88d8f89d 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1011,7 +1011,7 @@ let closure_of_filter evd evk = function
   | Some filter ->
   let evi = Evd.find_undefined evd evk in
   let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in
-  let test b decl = b || Idset.mem (get_id decl) vars ||
+  let test b decl = b || Id.Set.mem (get_id decl) vars ||
                     match decl with
                     | LocalAssum _ ->
                        false
@@ -1561,19 +1561,19 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
   let rhs = whd_beta evd rhs (* heuristic *) in
   let fast rhs = 
     let filter_ctxt = evar_filtered_context evi in
-    let names = ref Idset.empty in
+    let names = ref Id.Set.empty in
     let rec is_id_subst ctxt s =
       match ctxt, s with
       | (decl :: ctxt'), (c :: s') ->
         let id = get_id decl in
-        names := Idset.add id !names;
+        names := Id.Set.add id !names;
         isVarId evd id c && is_id_subst ctxt' s'
       | [], [] -> true
       | _ -> false 
     in
       is_id_subst filter_ctxt (Array.to_list argsv) &&
       closed0 evd rhs &&
-      Idset.subset (collect_vars evd rhs) !names 
+      Id.Set.subset (collect_vars evd rhs) !names 
   in
   let body =
     if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 1038945c1..fe134f512 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -88,7 +88,7 @@ let invert_tag cst tag reloc_tbl =
 let decompose_prod env t =
   let (name,dom,codom as res) = destProd (whd_all env t) in
   match name with
-  | Anonymous -> (Name (id_of_string "x"),dom,codom)
+  | Anonymous -> (Name (Id.of_string "x"),dom,codom)
   | _ -> res
 
 let app_type env c =
@@ -321,7 +321,7 @@ and nf_atom_type env sigma atom =
       mkCase(ci, p, a, branchs), tcase 
   | Afix(tt,ft,rp,s) ->
       let tt = Array.map (fun t -> nf_type env sigma t) tt in
-      let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in
+      let name = Array.map (fun _ -> (Name (Id.of_string "Ffix"))) tt in
       let lvl = nb_rel env in
       let nbfix = Array.length ft in
       let fargs = mk_rels_accu lvl (Array.length ft) in
@@ -334,7 +334,7 @@ and nf_atom_type env sigma atom =
       mkFix((rp,s),(name,tt,ft)), tt.(s)
   | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) ->
       let tt = Array.map (nf_type env sigma) tt in
-      let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in
+      let name = Array.map (fun _ -> (Name (Id.of_string "Fcofix"))) tt in
       let lvl = nb_rel env in
       let fargs = mk_rels_accu lvl (Array.length ft) in
       let env = push_rec_types (name,tt,[||]) env in
@@ -376,7 +376,7 @@ and  nf_predicate env sigma ind mip params v pT =
   | Vfun f, _ -> 
       let k = nb_rel env in
       let vb = f (mk_rel_accu k) 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 Int.equal n 0 then params else Array.map (lift n) params in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 30783bfad..a69caecab 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -202,7 +202,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
        with Not_found ->
 	 try
 	   let id = try Id.of_string s with _ -> raise Not_found in
-           evd, snd (Idmap.find id names)
+           evd, snd (Id.Map.find id names)
 	 with Not_found ->
 	   if not (is_strict_universe_declarations ()) then
   	     new_univ_level_variable ?loc ~name:s univ_rigid evd
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 708788ab8..9451b0f86 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1051,7 +1051,7 @@ let contextually byhead occs f env sigma t =
 let match_constr_evaluable_ref sigma c evref = 
   match EConstr.kind sigma c, evref with
   | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u
-  | Var id, EvalVarRef id' when id_eq id id' -> Some EInstance.empty
+  | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
   | _, _ -> None
 
 let substlin env sigma evalref n (nowhere_except_in,locs) c =
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index d4e9555f3..de9f8e700 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -97,7 +97,7 @@ val pr_glls   : goal list sigma -> Pp.t
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
   val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
-  val pf_global : identifier -> 'a Proofview.Goal.t -> Globnames.global_reference
+  val pf_global : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference
   (** FIXME: encapsulate the level in an existential type. *)
   val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
 
@@ -118,13 +118,13 @@ module New : sig
   val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types
   val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool
 
-  val pf_get_new_id  : identifier -> 'a Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+  val pf_get_new_id  : Id.t -> 'a Proofview.Goal.t -> Id.t
+  val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list
   val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t
-  val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
+  val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list
 
-  val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration
-  val pf_get_hyp_typ        : identifier -> 'a Proofview.Goal.t -> types
+  val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : Id.t -> 'a Proofview.Goal.t -> types
   val pf_last_hyp           : 'a Proofview.Goal.t -> named_declaration
 
   val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
diff --git a/stm/stm.ml b/stm/stm.ml
index 3cac3b609..6c22d3771 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -517,8 +517,8 @@ end = struct (* {{{ *)
   let reachable id = reachable !vcs id
   let mk_branch_name { expr = x } = Branch.make
     (let rec aux x = match x with
-    | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i
-    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i
+    | VernacDefinition (_,((_,i),_),_) -> Names.Id.to_string i
+    | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.Id.to_string i
     | VernacTime (_, e)
     | VernacTimeout (_, e) -> aux e
     | _ -> "branch" in aux x)
@@ -3097,7 +3097,7 @@ let current_proof_depth ~doc =
 let unmangle n =
   let n = VCS.Branch.to_string n in
   let idx = String.index n '_' + 1 in
-  Names.id_of_string (String.sub n idx (String.length n - idx))
+  Names.Id.of_string (String.sub n idx (String.length n - idx))
 
 let proofname b = match VCS.get_branch b with
   | { VCS.kind = (`Proof _| `Edit _) } -> Some b
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2b5bbfcd1..9097aebd0 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -439,7 +439,7 @@ let autounfolds db occs cls gl =
     in
     let (ids, csts) = Hint_db.unfolds db in
     let hyps = pf_ids_of_hyps gl in
-    let ids = Idset.filter (fun id -> List.mem id hyps) ids in
+    let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in
       Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
 	(Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
   in Proofview.V82.of_tactic (unfold_option unfolds cls) gl
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bce0dda10..07eea7b63 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -623,7 +623,7 @@ module New = struct
 	  let name_elim =
 	    match EConstr.kind sigma elim with
 	    | Const (kn, _) -> string_of_con kn
-	    | Var id -> string_of_id id
+	    | Var id -> Id.to_string id
 	    | _ -> "\b"
 	  in
 	  user_err ~hdr:"Tacticals.general_elim_then_using"
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2a04c413b..3abd42d46 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -226,12 +226,12 @@ module New : sig
 
   val nLastDecls  : 'a Proofview.Goal.t -> int -> named_context
 
-  val ifOnHyp     : (identifier * types -> bool) ->
-    (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
-    identifier -> unit Proofview.tactic
+  val ifOnHyp     : (Id.t * types -> bool) ->
+    (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) ->
+    Id.t -> unit Proofview.tactic
 
-  val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic
-  val onLastHypId      : (identifier -> unit tactic) -> unit tactic
+  val onNthHypId : int -> (Id.t -> unit tactic) -> unit tactic
+  val onLastHypId      : (Id.t -> unit tactic) -> unit tactic
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
@@ -239,9 +239,9 @@ module New : sig
                     (named_context -> unit tactic) -> unit tactic
   val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
 
-  val tryAllHyps          : (identifier -> unit tactic) -> unit tactic
-  val tryAllHypsAndConcl  : (identifier option -> unit tactic) -> unit tactic
-  val onClause   : (identifier option -> unit tactic) -> clause -> unit tactic
+  val tryAllHyps          : (Id.t -> unit tactic) -> unit tactic
+  val tryAllHypsAndConcl  : (Id.t option -> unit tactic) -> unit tactic
+  val onClause   : (Id.t option -> unit tactic) -> clause -> unit tactic
 
   val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family
   val elimination_sort_of_hyp  : Id.t -> 'a Proofview.Goal.t -> sorts_family
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f8f9e029b..6f67606d2 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1376,7 +1376,7 @@ let enforce_prop_bound_names rename tac =
                 (* "very_standard" says that we should have "H" names only, but
                    this would break compatibility even more... *)
                 let s = match Namegen.head_name sigma t with
-                  | Some id when not very_standard -> string_of_id id
+                  | Some id when not very_standard -> Id.to_string id
                   | _ -> "" in
                 Name (add_suffix Namegen.default_prop_ident s)
               else
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 32923ea81..98cf1b437 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -271,7 +271,7 @@ type eliminator = {
 val general_elim  : evars_flag -> clear_flag ->
   constr with_bindings -> eliminator -> unit Proofview.tactic
 
-val general_elim_clause : evars_flag -> unify_flags -> identifier option ->
+val general_elim_clause : evars_flag -> unify_flags -> Id.t option ->
   clausenv -> eliminator -> unit Proofview.tactic
 
 val default_elim  : evars_flag -> clear_flag -> constr with_bindings ->
@@ -355,7 +355,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic
 val assert_after  : Name.t -> types -> unit Proofview.tactic
 
 val assert_as     : (* true = before *) bool ->
-  (* optionally tell if a specialization of some hyp: *) identifier option ->
+  (* optionally tell if a specialization of some hyp: *) Id.t option ->
   intro_pattern option -> constr -> unit Proofview.tactic
 
 (** Implements the tactics assert, enough and pose proof; note that "by"
@@ -428,7 +428,7 @@ module Simple : sig
   val eapply : constr -> unit Proofview.tactic
   val elim   : constr -> unit Proofview.tactic
   val case   : constr -> unit Proofview.tactic
-  val apply_in : identifier -> constr -> unit Proofview.tactic
+  val apply_in : Id.t -> constr -> unit Proofview.tactic
 
 end
 
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 7af391758..66a4a2e49 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -190,7 +190,7 @@ let build_beq_scheme mode kn =
 	match EConstr.kind sigma c with
         | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
         | Var x ->
-          let eid = id_of_string ("eq_"^(string_of_id x)) in
+          let eid = Id.of_string ("eq_"^(Id.to_string x)) in
           let () =
             try ignore (Environ.lookup_named eid env)
             with Not_found -> raise (ParameterWithoutEquality (VarRef x))
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 9ab89c883..dbf7fec66 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -506,7 +506,7 @@ let save_proof ?proof = function
                   let env = Global.env () in
                   let ids_typ = Environ.global_vars_set env typ in
                   let ids_def = Environ.global_vars_set env pproof in
-                  Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
+                  Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
               | _ -> None in
 	    let decl = Proof_global.get_universe_decl () in
             let evd = Evd.from_ctx universes in