Merge PR #6972: [api] Deprecate a couple of aliases that we missed.

10 files changed, 15 insertions, 15 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index a2155697e..cb0fc3257 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -71,7 +71,7 @@ and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
-  | PROJ of projection * Declarations.projection_body * cbv_stack
+  | PROJ of Projection.t * Declarations.projection_body * cbv_stack
 
 (* les vars pourraient etre des constr,
    cela permet de retarder les lift: utile ?? *)
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 2ac59911c..cdaa39c53 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -41,7 +41,7 @@ and cbv_stack =
   | TOP
   | APP of cbv_value array * cbv_stack
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
-  | PROJ of projection * Declarations.projection_body * cbv_stack
+  | PROJ of Projection.t * Declarations.projection_body * cbv_stack
 
 val shift_value : int -> cbv_value -> cbv_value
 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 627430708..9270d6e3a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -38,7 +38,7 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -
 val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
 
 val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map
-(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *)
+[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"]
 
 (** Check all pending unification problems are solved and raise an
     error otherwise *)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 9b21599b6..3f05c58c4 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -63,7 +63,7 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env ->  evar_map ->
 val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result
 
 val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
-(** @deprecated Alias for [reconsider_unif_constraints] *)
+[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"]
 
 val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
   constr -> alias list option
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 296f25d3f..b0d714b03 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -129,8 +129,8 @@ val allowed_sorts : env -> inductive -> Sorts.family list
 val has_dependent_elim : mutual_inductive_body -> bool
 
 (** Primitive projections *)
-val projection_nparams : projection -> int
-val projection_nparams_env : env -> projection -> int
+val projection_nparams : Projection.t -> int
+val projection_nparams_env : env -> Projection.t -> int
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
 				     EConstr.t -> EConstr.types -> types
 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 9e3e68f05..360c6e86e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -275,12 +275,12 @@ sig
 
   type cst_member =
     | Cst_const of pconstant
-    | Cst_proj of projection
+    | Cst_proj of Projection.t
 
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * projection * Cst_stack.t
+  | Proj of int * int * Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
   and 'a t = 'a member list
@@ -332,12 +332,12 @@ struct
 
   type cst_member =
     | Cst_const of pconstant
-    | Cst_proj of projection
+    | Cst_proj of Projection.t
 
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * projection * Cst_stack.t
+  | Proj of int * int * Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int * int list * 'a t * Cst_stack.t
   and 'a t = 'a member list
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 29dc3ed0f..b8ac085a7 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -70,12 +70,12 @@ module Stack : sig
 
   type cst_member =
     | Cst_const of pconstant
-    | Cst_proj of projection
+    | Cst_proj of Projection.t
 
   type 'a member =
   | App of 'a app_node
   | Case of case_info * 'a * 'a array * Cst_stack.t
-  | Proj of int * int * projection * Cst_stack.t
+  | Proj of int * int * Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *)
     * 'a t * Cst_stack.t
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 40424ead4..2aff0c777 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -50,6 +50,6 @@ val type_of_global_reference_knowing_conclusion :
 
 val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list
 
-val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
+val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr
 
 val print_retype_error : retype_error -> Pp.t
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index fe83a2cc8..4905adf1f 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -55,4 +55,4 @@ val judge_of_abstraction : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment
 val judge_of_product : Environ.env -> Name.t ->
   unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment
-val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment
+val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f2f922fd5..ca03b96ab 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -466,7 +466,7 @@ let use_metas_pattern_unification sigma flags nb l =
 
 type key = 
   | IsKey of CClosure.table_key
-  | IsProj of projection * EConstr.constr
+  | IsProj of Projection.t * EConstr.constr
 
 let expand_table_key env = function
   | ConstKey cst -> constant_opt_value_in env cst