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

35 files changed, 67 insertions, 59 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 42629ced2..c4b00d0dc 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -104,7 +104,7 @@ type constr =
   | Case      of case_info * constr * constr * constr array
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
-  | Proj      of projection * constr
+  | Proj      of Projection.t * constr
 
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
diff --git a/checker/closure.ml b/checker/closure.ml
index 184af0e13..bfba6c161 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -251,7 +251,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 *)
@@ -281,7 +281,7 @@ let update v1 (no,t) =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * projection
+  | Zproj of int * int * Projection.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/closure.mli b/checker/closure.mli
index f68c0468a..4cf02ae2b 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -87,7 +87,7 @@ type 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 *)
@@ -107,7 +107,7 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * projection
+  | Zproj of int * int * Projection.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/environ.mli b/checker/environ.mli
index 36e0ea027..81da83875 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -58,7 +58,7 @@ val constant_value : env -> Constant.t puniverses -> constr
 val evaluable_constant : Constant.t -> env -> bool
 
 val is_projection : Constant.t -> env -> bool
-val lookup_projection : projection -> env -> projection_body
+val lookup_projection : Projection.t -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 97255dd49..072dec63f 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -54,7 +54,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.projection * lift
+  | Zlproj of Names.Projection.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -142,7 +142,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-	       if not (Names.eq_con_chk
+               if not (Names.Constant.UserOrd.equal
 		       (Names.Projection.constant c1)
 		       (Names.Projection.constant c2)) then 
 		raise NotConvertible
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index ee73eb1ab..5cb38cb81 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -224,7 +224,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     | Some None, Some None -> true
     | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
       Id.equal id1 id2 &&
-      Array.for_all2 eq_con_chk p1 p2 &&
+      Array.for_all2 Constant.UserOrd.equal p1 p2 &&
       Array.for_all2 eq_projection_body pb1 pb2
     | _, _ -> false
   in
diff --git a/checker/term.ml b/checker/term.ml
index 19034a57d..0236f7867 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -390,7 +390,7 @@ let compare_constr f t1 t2 =
           f h1 h2 && List.for_all2 f l1 l2
         else false
   | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
-  | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2
+  | Const c1, Const c2 -> eq_puniverses Constant.UserOrd.equal c1 c2
   | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2
   | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2
     && Univ.Instance.equal u1 u2
diff --git a/checker/values.ml b/checker/values.ml
index 160653d9b..1ac8d7cef 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 2c3436106636784886f122c8ab578098 checker/cic.mli
+MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli
 
 *)
 
diff --git a/clib/cArray.ml b/clib/cArray.ml
index 5eb20bc16..071f4689b 100644
--- a/clib/cArray.ml
+++ b/clib/cArray.ml
@@ -62,9 +62,12 @@ sig
   val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array
   val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
+  [@@ocaml.deprecated "Same as [fold_left_map]"]
   val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
+  [@@ocaml.deprecated "Same as [fold_right_map]"]
   val fold_map2' :
     ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
+  [@@ocaml.deprecated "Same as [fold_right2_map]"]
   val distinct : 'a array -> bool
   val rev_of_list : 'a list -> 'a array
   val rev_to_list : 'a array -> 'a list
diff --git a/clib/cArray.mli b/clib/cArray.mli
index f4f60f8aa..9c2f521f4 100644
--- a/clib/cArray.mli
+++ b/clib/cArray.mli
@@ -114,14 +114,14 @@ sig
   (** Same with two arrays, folding on the left *)
 
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array
-  (** @deprecated Same as [fold_left_map] *)
+  [@@ocaml.deprecated "Same as [fold_left_map]"]
 
   val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c
-  (** @deprecated Same as [fold_right_map] *)
+  [@@ocaml.deprecated "Same as [fold_right_map]"]
 
   val fold_map2' :
     ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c
-  (** @deprecated Same as [fold_right2_map] *)
+  [@@ocaml.deprecated "Same as [fold_right2_map]"]
 
   val distinct : 'a array -> bool
   (** Return [true] if every element of the array is unique (for default 
diff --git a/clib/cList.ml b/clib/cList.ml
index 80bb18477..8727f4696 100644
--- a/clib/cList.ml
+++ b/clib/cList.ml
@@ -102,7 +102,9 @@ sig
   val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list
   val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
+  [@@ocaml.deprecated "Same as [fold_left_map]"]
   val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
+  [@@ocaml.deprecated "Same as [fold_right_map]"]
   val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
   val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
   val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list
diff --git a/clib/cList.mli b/clib/cList.mli
index db37050aa..fd6d6a158 100644
--- a/clib/cList.mli
+++ b/clib/cList.mli
@@ -228,11 +228,10 @@ sig
   (** Same with four lists, folding on the left *)
 
   val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list
-  (* [@@ocaml.deprecated "Same as [fold_left_map]"] *)
-  (** @deprecated Same as [fold_left_map] *)
+  [@@ocaml.deprecated "Same as [fold_left_map]"]
 
   val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a
-  (** @deprecated Same as [fold_right_map] *)
+  [@@ocaml.deprecated "Same as [fold_right_map]"]
 
   val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
   val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b
diff --git a/clib/option.mli b/clib/option.mli
index 67b42268a..14fa9da38 100644
--- a/clib/option.mli
+++ b/clib/option.mli
@@ -98,6 +98,7 @@ val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b option -> 'a -> 'c option * 'a
 
 (** @deprecated Same as [fold_left_map] *)
 val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option
+[@@ocaml.deprecated "Same as [fold_left_map]"]
 
 (** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *)
 val cata : ('a -> 'b) -> 'b -> 'a option -> 'b
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 28c9dd3c2..8ee3b9050 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -108,7 +108,7 @@ val mkLetIn : Name.t * t * t * t -> t
 val mkApp : t * t array -> t
 val mkConst : Constant.t -> t
 val mkConstU : Constant.t * EInstance.t -> t
-val mkProj : (projection * t) -> t
+val mkProj : (Projection.t * t) -> t
 val mkInd : inductive -> t
 val mkIndU : inductive * EInstance.t -> t
 val mkConstruct : constructor -> t
@@ -173,7 +173,7 @@ val destEvar : Evd.evar_map -> t -> t pexistential
 val destInd : Evd.evar_map -> t -> inductive * EInstance.t
 val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t
 val destCase : Evd.evar_map -> t -> case_info * t * t * t array
-val destProj : Evd.evar_map -> t -> projection * t
+val destProj : Evd.evar_map -> t -> Projection.t * t
 val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
 val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
 
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 1eeb8e41a..103a4f9e9 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -130,7 +130,7 @@ val make_implicits_list : implicit_status list -> implicits_list list
 
 val drop_first_implicits : int -> implicits_list -> implicits_list
 
-val projection_implicits : env -> projection -> implicit_status list -> 
+val projection_implicits : env -> Projection.t -> implicit_status list ->
   implicit_status list
 
 val select_impargs_size : int -> implicits_list list -> implicit_status list
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index aa9a6ed0d..a76f82094 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -210,7 +210,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
       let e',na = protect g e na in
       GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
   | NRec (fk,idl,dll,tl,bl) ->
-      let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) ->
+      let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) ->
           let e,na = protect g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = Array.fold_left_map (to_id (protect g)) e idl in
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
 
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