diff options
| author | Maxime Dénès | 2016-09-05 17:50:27 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-05 17:53:09 +0200 |
| commit | 47a2da7326ed975039f9e94780aeb9b1079f4854 (patch) | |
| tree | 49dbc887b617b86d1aa15fb04c84ebbc5a9e6d1e /kernel/nativecode.ml | |
| parent | 52b82dd42b93af6831df3bfea4822c6c8680a288 (diff) | |
Fix #5065: Anomaly: Not a proof by induction
Using abstract can create beta-redexes or let-ins in the head of the
proof terms. The code projecting out mutual lemmas was not robust
enough.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions