[api] Deprecate a couple of aliases that we missed.

8 files changed, 11 insertions, 11 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
 
 *)