diff options
| author | Maxime Dénès | 2018-01-24 13:22:19 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-01-24 13:58:22 +0100 |
| commit | e8fbc417cb1d2f63a0ec33cb967b7e0258084d48 (patch) | |
| tree | f5eb7cf61278bf1848655a039016594f5a27741d /kernel/nativecode.ml | |
| parent | 2e798fb83db743ce44350af6f7f9442811f374ad (diff) | |
Fix #6621: Anomaly on fixpoint with primitive projections
The implementation of the subterm relation for primitive projections was
a bit wrong. I found the problem independently of this bug, and tried to
see if a proof of False could be derived, but I don't think so, due to
another check (check_is_subterm) that saves the kernel at the last
minute.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions