diff options
| author | Hugo Herbelin | 2015-09-08 11:25:00 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-09-08 13:49:55 +0200 |
| commit | f899f861fc82de7eb7241071d602eb15b68b7a1d (patch) | |
| tree | 82f7f9a07398d045d493f294e4d6a50fb348ee30 /kernel/nativelambda.ml | |
| parent | 76f27140e6e3465b2d4086653bccae5206b3cfb6 (diff) | |
New option "Unset Bracketing Last Introduction Pattern" for preserving
compatibility with the non uniform behavior that "intros [] []" on
"A*B->C*D->E" automatically introduces A and B but leaves C and D in
the goal.
Kept unset in 8.5 but planned to be set in 8.6.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions