diff options
| author | Hugo Herbelin | 2015-01-24 21:27:54 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-24 22:27:57 +0100 |
| commit | 0e06c54a9249477fdab5b135ffdac4bd3ea501a5 (patch) | |
| tree | 71d5cc86ab1d09f6fed685319a734d45661b839f /kernel/nativelambda.mli | |
| parent | 14787df2ea09994151e886bf918aca0aecbd8ade (diff) | |
Removed obsolete option "Legacy Partially Applied Elimination
Argument" which I used temporarily in a branch to have "destruct eq_dec"
working like in v8.4 and not like the "destruct (eq_dec _ _)"
of 8.4. I finally made "destruct (eq_dec _ _)" working in 8.5 like
"destruct eq_dec" was working in 8.4 (and is still working in 8.5).
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions