diff options
| author | Pierre-Marie Pédrot | 2019-06-16 17:03:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-16 17:03:29 +0200 |
| commit | 3ca9529b5fdbb8e2a3dc18e38862cbe351e8e0e0 (patch) | |
| tree | 975eb71258f604af95a525522d29cfe856789391 /kernel/nativecode.ml | |
| parent | 5d58496c27fc5767c7841734c0f01a739cf529ab (diff) | |
Fix #10090: Ltac1 destruct and Ltac2 destruct should do the same thing.
The ML wrapper was wrongly calling induction instead of destruct.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions