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

9 files changed, 26 insertions, 23 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 5f683790c..08114abc4 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -96,7 +96,7 @@ module type RedFlagsSig = sig
   val red_transparent : reds -> transparent_state
   val mkflags : red_kind list -> reds
   val red_set : reds -> red_kind -> bool
-  val red_projection : reds -> projection -> bool
+  val red_projection : reds -> Projection.t -> bool
 end
 
 module RedFlags = (struct
@@ -364,7 +364,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of projection * fconstr
+  | FProj of Projection.t * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 3a7f77d52..e2f5a3b82 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -74,7 +74,7 @@ module type RedFlagsSig = sig
 
   (** This tests if the projection is in unfolded state already or
       is unfodable due to delta. *)
-  val red_projection : reds -> projection -> bool
+  val red_projection : reds -> Projection.t -> bool
 end
 
 module RedFlags : RedFlagsSig
@@ -132,7 +132,7 @@ type fterm =
   | FInd of inductive Univ.puniverses
   | FConstruct of constructor Univ.puniverses
   | FApp of fconstr * fconstr array
-  | FProj of projection * fconstr
+  | FProj of Projection.t * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
diff --git a/kernel/constr.ml b/kernel/constr.ml
index ba7fecadf..4f062d72f 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -100,7 +100,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of projection * 'constr
+  | Proj      of Projection.t * 'constr
 (* constr is the fixpoint of the previous type. Requires option
    -rectypes of the Caml compiler to be set *)
 type t = (t, t, Sorts.t, Instance.t) kind_of_term
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 98c0eaa28..0d464840c 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -122,7 +122,7 @@ val mkConst : Constant.t -> constr
 val mkConstU : pconstant -> constr
 
 (** Constructs a projection application *)
-val mkProj : (projection * constr) -> constr
+val mkProj : (Projection.t * constr) -> constr
 
 (** Inductive types *)
 
@@ -220,7 +220,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of projection * 'constr
+  | Proj      of Projection.t * 'constr
 
 (** User view of [constr]. For [App], it is ensured there is at
    least one argument and the function is not itself an applicative
@@ -318,7 +318,7 @@ where [info] is pretty-printing information *)
 val destCase : constr -> case_info * constr * constr * constr array
 
 (** Destructs a projection *)
-val destProj : constr -> projection * constr
+val destProj : constr -> Projection.t * constr
 
 (** Destructs the {% $ %}i{% $ %}th function of the block
    [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1}
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 4e6ac1e72..fdd84b25b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -168,7 +168,7 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option
 
 (** {6 Primitive projections} *)
 
-val lookup_projection    : Names.projection -> env -> projection_body
+val lookup_projection    : Names.Projection.t -> env -> projection_body
 val is_projection : Constant.t -> env -> bool
 
 (** {5 Inductive types } *)
diff --git a/kernel/names.mli b/kernel/names.mli
index ffd96781b..96e020aed 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -547,6 +547,8 @@ val eq_constant_key : Constant.t -> Constant.t -> bool
 (** equalities on constant and inductive names (for the checker) *)
 
 val eq_con_chk : Constant.t -> Constant.t -> bool
+[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."]
+
 val eq_ind_chk : inductive -> inductive -> bool
 
 (** {6 Deprecated functions. For backward compatibility.} *)
@@ -633,27 +635,27 @@ val eq_label : Label.t -> Label.t -> bool
 (** {5 Unique bound module names} *)
 
 type mod_bound_id = MBId.t
-(** Alias type. *)
+[@@ocaml.deprecated "Same as [MBId.t]."]
 
-val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+val mod_bound_id_ord : MBId.t -> MBId.t -> int
 [@@ocaml.deprecated "Same as [MBId.compare]."]
 
-val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
+val mod_bound_id_eq : MBId.t -> MBId.t -> bool
 [@@ocaml.deprecated "Same as [MBId.equal]."]
 
-val make_mbid : DirPath.t -> Id.t -> mod_bound_id
+val make_mbid : DirPath.t -> Id.t -> MBId.t
 [@@ocaml.deprecated "Same as [MBId.make]."]
 
-val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t
+val repr_mbid : MBId.t -> int * Id.t * DirPath.t
 [@@ocaml.deprecated "Same as [MBId.repr]."]
 
-val id_of_mbid : mod_bound_id -> Id.t
+val id_of_mbid : MBId.t -> Id.t
 [@@ocaml.deprecated "Same as [MBId.to_id]."]
 
-val string_of_mbid : mod_bound_id -> string
+val string_of_mbid : MBId.t -> string
 [@@ocaml.deprecated "Same as [MBId.to_string]."]
 
-val debug_string_of_mbid : mod_bound_id -> string
+val debug_string_of_mbid : MBId.t -> string
 [@@ocaml.deprecated "Same as [MBId.debug_to_string]."]
 
 (** {5 Names} *)
@@ -745,6 +747,7 @@ module Projection : sig
 end
 
 type projection = Projection.t
+[@@ocaml.deprecated "Alias for [Projection.t]"]
 
 val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t
 [@@ocaml.deprecated "Same as [Constant.make]"]
diff --git a/kernel/term.ml b/kernel/term.ml
index 403ed881c..e1affb1c0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of projection * 'constr
+  | Proj      of Projection.t * 'constr
 
 type values = Vmvalues.values
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 7cb3b662d..ee84dcb2b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -155,7 +155,7 @@ val destCase : constr -> case_info * constr * constr * constr array
 [@@ocaml.deprecated "Alias for [Constr.destCase]"]
 
 (** Destructs a projection *)
-val destProj : constr -> projection * constr
+val destProj : constr -> Projection.t * constr
 [@@ocaml.deprecated "Alias for [Constr.destProj]"]
 
 (** Destructs the {% $ %}i{% $ %}th function of the block
@@ -403,7 +403,7 @@ val mkApp : constr * constr array -> constr
 [@@ocaml.deprecated "Alias for Constr"]
 val mkConst : Constant.t -> constr
 [@@ocaml.deprecated "Alias for Constr"]
-val mkProj : projection * constr -> constr
+val mkProj : Projection.t * constr -> constr
 [@@ocaml.deprecated "Alias for Constr"]
 val mkInd : inductive -> constr
 [@@ocaml.deprecated "Alias for Constr"]
@@ -571,7 +571,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Case      of Constr.case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) Constr.pfixpoint
   | CoFix     of ('constr, 'types) Constr.pcofixpoint
-  | Proj      of projection * 'constr
+  | Proj      of Projection.t * 'constr
 [@@ocaml.deprecated "Alias for Constr.kind_of_term"]
 
 type values = Vmvalues.values
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index bff40b017..85b2cfffd 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -60,7 +60,7 @@ val judge_of_constant : env -> pconstant -> unsafe_judgment
 
 (** {6 type of an applied projection } *)
 
-val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment
+val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment
 
 (** {6 Type of application. } *)
 val judge_of_apply :
@@ -100,7 +100,7 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-val type_of_projection_constant : env -> Names.projection puniverses -> types
+val type_of_projection_constant : env -> Projection.t puniverses -> types
 
 val type_of_constant_in : env -> pconstant -> types