diff options
| author | Maxime Dénès | 2015-02-26 09:58:46 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2015-02-26 09:58:46 +0100 |
| commit | 9dacc590c604290d9556d9368c5c735321e01e90 (patch) | |
| tree | 887fd2572a386adca5148619ca8f7b09caac6374 /kernel/nativelambda.ml | |
| parent | d82f2c96e73484aae7e6f9e014823065584fbc6e (diff) | |
Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."
This reverts commit 4e6c9891140932f452bb5ac8960d597b0b5fde1d, which was
breaking compatibility because one could no longer use names of foralls in
the goal without introducting them. Probably not good style, but it did
break many existing developments including CompCert.
Closes #4093 but reopens #4035.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions