[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, 14 insertions, 14 deletions

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