diff options
| author | Pierre-Marie Pédrot | 2019-03-19 00:22:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-04 14:01:46 +0100 |
| commit | b6d5332c6e3127ba3fec466abe502ee40c031ed2 (patch) | |
| tree | ab6d83f378941af347d0aaf387d4f42ed7651608 /kernel/constr.ml | |
| parent | fd50f21cfe2460fa35fe962390f4ba810d7ca837 (diff) | |
Fix behaviour of destruct after change of case representation.
We ensure not to generate dummy beta-cuts in case branches generated
by destruct. There was seemingly code trying to perform this but in
an akward way.
Diffstat (limited to 'kernel/constr.ml')
0 files changed, 0 insertions, 0 deletions