[api] Deprecate all legacy uses of Names in core.

This will allow to merge back `Names` with `API.Names`

5 files changed, 12 insertions, 12 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c03a3ba6..881000219 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -374,16 +374,16 @@ let find_elim hdcncl lft2rgt dep cls ot =
         | Some true, None
         | Some false, Some _ ->
 	  let c1 = destConstRef pr1 in 
-	  let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in 
+	  let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in 
 	  let l' = Label.of_id (add_suffix (Label.to_id l) "_r")  in 
-	  let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in
+	  let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in
 	  begin 
 	    try 
 	      let _ = Global.lookup_constant c1' in
 		c1'
 	    with Not_found -> 
 	      user_err ~hdr:"Equality.find_elim"
-                (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".")
+                (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
 	  end
 	| _ -> destConstRef pr1
         end
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 7f087ea01..240b5a7e0 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -29,7 +29,7 @@ open Pp
 (* Registering schemes in the environment *)
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
   internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
@@ -57,7 +57,7 @@ let discharge_scheme (_,(kind,l)) =
   Some (kind,Array.map (fun (ind,const) ->
     (Lib.discharge_inductive ind,Lib.discharge_con const)) l)
 
-let inScheme : string * (inductive * constant) array -> obj =
+let inScheme : string * (inductive * Constant.t) array -> obj =
   declare_object {(default_object "SCHEME") with
                     cache_function = cache_scheme;
                     load_function = (fun _ -> cache_scheme);
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index f825c4f4a..232a193ac 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -20,7 +20,7 @@ type individual
 type 'a scheme_kind
 
 type mutual_scheme_object_function =
-  internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
+  internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants
 type individual_scheme_object_function =
   internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants
 
@@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string ->
 
 val define_individual_scheme : individual scheme_kind -> 
   internal_flag (** internal *) ->
-  Id.t option -> inductive -> constant * Safe_typing.private_constants
+  Id.t option -> inductive -> Constant.t * Safe_typing.private_constants
 
 val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) ->
-  (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants
+  (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants
 
 (** Main function to retrieve a scheme in the cache or to generate it *)
-val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants
+val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants
 
 val check_scheme : 'a scheme_kind -> inductive -> bool
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 07eea7b63..fe733899f 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -622,7 +622,7 @@ module New = struct
       | _ ->
 	  let name_elim =
 	    match EConstr.kind sigma elim with
-	    | Const (kn, _) -> string_of_con kn
+	    | Const (kn, _) -> Constant.to_string kn
 	    | Var id -> Id.to_string id
 	    | _ -> "\b"
 	  in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f67606d2..866daa904 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -580,7 +580,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl ->
   | (f, n, ar) :: oth ->
     let open Context.Named.Declaration in
     let (sp', u')  = check_mutind env sigma n ar in
-    if not (eq_mind sp sp') then
+    if not (MutInd.equal sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
     if mem_named_context_val f sign then
       user_err ~hdr:"Logic.prim_refiner"
@@ -1607,7 +1607,7 @@ let general_elim_clause with_evars flags id c e =
 (* Apply a tactic below the products of the conclusion of a lemma *)
 
 type conjunction_status =
-  | DefinedRecord of constant option list
+  | DefinedRecord of Constant.t option list
   | NotADefinedRecordUseScheme of constr
 
 let make_projection env sigma params cstr sign elim i n c u =