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

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

5 files changed, 11 insertions, 11 deletions

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 =