diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:08:04 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2018-06-04 14:08:04 +0200 |
| commit | 1757f89b6c61024bbe3aebd6b43c56df0d92f5eb (patch) | |
| tree | 3a04f1f948df72be5d58ae992508e303128db23d /checker | |
| parent | 10e323fe4cebd1addfe1af32407f1277214d2c7b (diff) | |
| parent | 3be70f39bbaba7c7edb5e5f3e26d4f952c06824e (diff) | |
Merge PR #7552: Fix #7539: Checker does not properly handle negative coinductive types.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/closure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/closure.ml b/checker/closure.ml index 66e69f225..b9ae4daa8 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -754,7 +754,7 @@ let rec knr info m stk = | (_,args,s) -> (m,args@s)) | FCoFix _ when red_set info.i_flags fIOTA -> (match strip_update_shift_app m stk with - (_, args, (((ZcaseT _)::_) as stk')) -> + (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in knit info fxe fxbd (args@stk') | (_,args,s) -> (m,args@s)) |