diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-02 20:18:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-12-02 20:31:54 +0100 |
| commit | fdcee15907f2cff920ba6b27d9076ca47db26150 (patch) | |
| tree | 2fcac5baabab93ee4d4079aec2bbf233b4c724a2 /checker/closure.mli | |
| parent | 0048cbe810c82a775558c14cd7fcae644e205c51 (diff) | |
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.
Diffstat (limited to 'checker/closure.mli')
| -rw-r--r-- | checker/closure.mli | 2 |
1 files changed, 0 insertions, 2 deletions
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 |