diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-18 16:00:17 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-18 16:03:41 +0200 |
| commit | 3be70f39bbaba7c7edb5e5f3e26d4f952c06824e (patch) | |
| tree | aa27a2caa4d11f3431a0768e9c1edb916fd35174 /checker | |
| parent | a0da3a68d12141ba226ce94027b90a01389099d0 (diff) | |
Fix #7539: Checker does not properly handle negative coinductive types.
The reduction machine of the checker was not taking into account the fact
that cofixpoints needed to be unfolded when applied against a projection.
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 bfba6c161..3f6dfd30f 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -762,7 +762,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)) |