From fdcee15907f2cff920ba6b27d9076ca47db26150 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 2 Dec 2017 20:18:10 +0100 Subject: Remove redundant Zcase from the checker. This was redundant with ZcaseT, the only difference lying in the use or not of fclosures for substerms. This code was removed from the kernel in commit f2f805ed, we finish the work in the checker now. --- checker/closure.mli | 2 -- 1 file changed, 2 deletions(-) (limited to 'checker/closure.mli') diff --git a/checker/closure.mli b/checker/closure.mli index 957cc4adb..02d8b22fa 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -98,7 +98,6 @@ type fterm = | FProj of projection * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs - | FCase of case_info * fconstr * fconstr * fconstr array | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) | FLambda of int * (Name.t * constr) list * constr * fconstr subs | FProd of Name.t * fconstr * fconstr @@ -115,7 +114,6 @@ type fterm = type stack_member = | Zapp of fconstr array - | Zcase of case_info * fconstr * fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs | Zproj of int * int * projection | Zfix of fconstr * stack -- cgit v1.2.3