From 0ade32f84b28d2190360ec79520788142755b5b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Mar 2018 20:29:16 +0100 Subject: [api] Deprecate a couple of aliases that we missed. --- checker/cic.mli | 2 +- checker/closure.ml | 4 ++-- checker/closure.mli | 4 ++-- checker/environ.mli | 2 +- checker/reduction.ml | 4 ++-- checker/subtyping.ml | 2 +- checker/term.ml | 2 +- checker/values.ml | 2 +- 8 files changed, 11 insertions(+), 11 deletions(-) (limited to 'checker') 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 *) -- cgit v1.2.3