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

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

1 files changed, 25 insertions, 25 deletions

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index f1d0e4279..1d7012ce5 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -20,44 +20,44 @@ type delta_resolver
 val empty_delta_resolver : delta_resolver
 
 val add_mp_delta_resolver :
-  module_path -> module_path -> delta_resolver -> delta_resolver
+  ModPath.t -> ModPath.t -> delta_resolver -> delta_resolver
 
 val add_kn_delta_resolver :
-  kernel_name -> kernel_name -> delta_resolver -> delta_resolver
+  KerName.t -> KerName.t -> delta_resolver -> delta_resolver
 
 val add_inline_delta_resolver :
-  kernel_name -> (int * constr option) -> delta_resolver -> delta_resolver
+  KerName.t -> (int * constr option) -> delta_resolver -> delta_resolver
 
 val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
 
 (** Effect of a [delta_resolver] on a module path, on a kernel name *)
 
-val mp_of_delta : delta_resolver -> module_path -> module_path
-val kn_of_delta : delta_resolver -> kernel_name -> kernel_name
+val mp_of_delta : delta_resolver -> ModPath.t -> ModPath.t
+val kn_of_delta : delta_resolver -> KerName.t -> KerName.t
 
 (** Build a constant whose canonical part is obtained via a resolver *)
 
-val constant_of_delta_kn : delta_resolver -> kernel_name -> constant
+val constant_of_delta_kn : delta_resolver -> KerName.t -> Constant.t
 
 (** Same, but a 2nd resolver is tried if the 1st one had no effect *)
 
 val constant_of_deltas_kn :
-  delta_resolver -> delta_resolver -> kernel_name -> constant
+  delta_resolver -> delta_resolver -> KerName.t -> Constant.t
 
 (** Same for inductive names *)
 
-val mind_of_delta_kn : delta_resolver -> kernel_name -> mutual_inductive
+val mind_of_delta_kn : delta_resolver -> KerName.t -> MutInd.t
 val mind_of_deltas_kn :
-  delta_resolver -> delta_resolver -> kernel_name -> mutual_inductive
+  delta_resolver -> delta_resolver -> KerName.t -> MutInd.t
 
 (** Extract the set of inlined constant in the resolver *)
-val inline_of_delta : int option -> delta_resolver -> (int * kernel_name) list
+val inline_of_delta : int option -> delta_resolver -> (int * KerName.t) list
 
 (** Does a [delta_resolver] contains a [mp], a constant, an inductive ? *)
 
-val mp_in_delta : module_path -> delta_resolver -> bool
-val con_in_delta : constant -> delta_resolver -> bool
-val mind_in_delta : mutual_inductive -> delta_resolver -> bool
+val mp_in_delta : ModPath.t -> delta_resolver -> bool
+val con_in_delta : Constant.t -> delta_resolver -> bool
+val mind_in_delta : MutInd.t -> delta_resolver -> bool
 
 
 (** {6 Substitution} *)
@@ -72,15 +72,15 @@ val is_empty_subst : substitution -> bool
    composition. Most often this is not what you want. For sequential
    composition, try [join (map_mbid mp delta) subs] **)
 val add_mbid :
-  MBId.t -> module_path -> delta_resolver  -> substitution -> substitution
+  MBId.t -> ModPath.t -> delta_resolver  -> substitution -> substitution
 val add_mp :
-  module_path -> module_path -> delta_resolver -> substitution -> substitution
+  ModPath.t -> ModPath.t -> delta_resolver -> substitution -> substitution
 
 (** map_* create a new substitution [arg2/arg1]\{arg3\} *)
 val map_mbid :
-  MBId.t -> module_path -> delta_resolver -> substitution
+  MBId.t -> ModPath.t -> delta_resolver -> substitution
 val map_mp :
-  module_path -> module_path -> delta_resolver -> substitution
+  ModPath.t -> ModPath.t -> delta_resolver -> substitution
 
 (** sequential composition:
    [substitute (join sub1 sub2) t = substitute sub2 (substitute sub1 t)]
@@ -117,10 +117,10 @@ val debug_pr_delta : delta_resolver -> Pp.t
    as well [==] *)
 
 val subst_mp :
-  substitution -> module_path -> module_path
+  substitution -> ModPath.t -> ModPath.t
 
 val subst_mind :
-  substitution -> mutual_inductive -> mutual_inductive
+  substitution -> MutInd.t -> MutInd.t
 
 val subst_ind :
   substitution -> inductive -> inductive
@@ -128,10 +128,10 @@ val subst_ind :
 val subst_pind : substitution -> pinductive -> pinductive
 
 val subst_kn :
-  substitution -> kernel_name -> kernel_name
+  substitution -> KerName.t -> KerName.t
 
 val subst_con :
-  substitution -> pconstant -> constant * constr
+  substitution -> pconstant -> Constant.t * constr
 
 val subst_pcon :
   substitution -> pconstant -> pconstant
@@ -140,10 +140,10 @@ val subst_pcon_term :
   substitution -> pconstant -> pconstant * constr
 
 val subst_con_kn :
-  substitution -> constant -> constant * constr
+  substitution -> Constant.t -> Constant.t * constr
 
-val subst_constant : 
-  substitution -> constant -> constant
+val subst_constant :
+  substitution -> Constant.t -> Constant.t
 
 (** Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
@@ -154,7 +154,7 @@ val subst_evaluable_reference :
   substitution -> evaluable_global_reference -> evaluable_global_reference
 
 (** [replace_mp_in_con mp mp' con] replaces [mp] with [mp'] in [con] *)
-val replace_mp_in_kn : module_path -> module_path -> kernel_name -> kernel_name
+val replace_mp_in_kn : ModPath.t -> ModPath.t -> KerName.t -> KerName.t
 
 (** [subst_mps sub c] performs the substitution [sub] on all kernel
    names appearing in [c] *)