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 /vernac/topfmt.mli | |
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 'vernac/topfmt.mli')
0 files changed, 0 insertions, 0 deletions