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

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

1 files changed, 20 insertions, 20 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2667ad7ca..37816f1e5 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -126,19 +126,19 @@ val pop_rel_context : int -> env -> env
 (** {5 Global constants }
   {6 Add entries to global environment } *)
 
-val add_constant : constant -> constant_body -> env -> env
-val add_constant_key : constant -> constant_body -> Pre_env.link_info ->
+val add_constant : Constant.t -> constant_body -> env -> env
+val add_constant_key : Constant.t -> constant_body -> Pre_env.link_info ->
   env -> env
 
 (** Looks up in the context of global constant names 
    raises [Not_found] if the required path is not found *)
-val lookup_constant    : constant -> env -> constant_body
-val evaluable_constant : constant -> env -> bool
+val lookup_constant    : Constant.t -> env -> constant_body
+val evaluable_constant : Constant.t -> env -> bool
 
 (** New-style polymorphism *)
-val polymorphic_constant  : constant -> env -> bool
+val polymorphic_constant  : Constant.t -> env -> bool
 val polymorphic_pconstant : pconstant -> env -> bool
-val type_in_type_constant : constant -> env -> bool
+val type_in_type_constant : Constant.t -> env -> bool
 
 (** {6 ... } *)
 (** [constant_value env c] raises [NotEvaluableConst Opaque] if
@@ -149,35 +149,35 @@ val type_in_type_constant : constant -> env -> bool
 type const_evaluation_result = NoBody | Opaque | IsProj
 exception NotEvaluableConst of const_evaluation_result
 
-val constant_value : env -> constant puniverses -> constr constrained
-val constant_type : env -> constant puniverses -> types constrained
+val constant_value : env -> Constant.t puniverses -> constr constrained
+val constant_type : env -> Constant.t puniverses -> types constrained
 
-val constant_opt_value : env -> constant puniverses -> (constr * Univ.constraints) option
-val constant_value_and_type : env -> constant puniverses -> 
+val constant_opt_value : env -> Constant.t puniverses -> (constr * Univ.constraints) option
+val constant_value_and_type : env -> Constant.t puniverses -> 
   constr option * types * Univ.constraints
 (** The universe context associated to the constant, empty if not 
     polymorphic *)
-val constant_context : env -> constant -> Univ.abstract_universe_context
+val constant_context : env -> Constant.t -> Univ.abstract_universe_context
 
 (* These functions should be called under the invariant that [env] 
    already contains the constraints corresponding to the constant 
    application. *)
-val constant_value_in : env -> constant puniverses -> constr
-val constant_type_in : env -> constant puniverses -> types
-val constant_opt_value_in : env -> constant puniverses -> constr option
+val constant_value_in : env -> Constant.t puniverses -> constr
+val constant_type_in : env -> Constant.t puniverses -> types
+val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 (** {6 Primitive projections} *)
 
 val lookup_projection    : Names.projection -> env -> projection_body
-val is_projection : constant -> env -> bool
+val is_projection : Constant.t -> env -> bool
 
 (** {5 Inductive types } *)
-val add_mind_key : mutual_inductive -> Pre_env.mind_key -> env -> env
-val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
+val add_mind_key : MutInd.t -> Pre_env.mind_key -> env -> env
+val add_mind : MutInd.t -> mutual_inductive_body -> env -> env
 
 (** Looks up in the context of global inductive names 
    raises [Not_found] if the required path is not found *)
-val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
+val lookup_mind : MutInd.t -> env -> mutual_inductive_body
 
 (** New-style polymorphism *)
 val polymorphic_ind  : inductive -> env -> bool
@@ -195,8 +195,8 @@ val add_modtype : module_type_body -> env -> env
 (** [shallow_add_module] does not add module components *)
 val shallow_add_module : module_body -> env -> env
 
-val lookup_module : module_path -> env -> module_body
-val lookup_modtype : module_path -> env -> module_type_body
+val lookup_module : ModPath.t -> env -> module_body
+val lookup_modtype : ModPath.t -> env -> module_type_body
 
 (** {5 Universe constraints } *)