diff options
| author | Gaëtan Gilbert | 2019-10-31 13:17:15 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-31 13:22:50 +0100 |
| commit | 3910e8dca2154d15c422a8e5ceb16f93c5faf889 (patch) | |
| tree | 70de268936141d67a5e596868619175538b4d18a /dev/ci | |
| parent | 43bd5e05ddd23378fc9d2f82a07a4e3153819521 (diff) | |
Fix #8459: anomaly not enough abstractions in fix body
We reach the anomaly because we call check_fix on a surrounding
fixpoint from the pretyper, and the inner fix hasn't been checked.
Using whd_all isn't useful in the specific reported case but a case
where it's necessary can probably be crafted.
See also #11013
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions