diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-02-24 00:27:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-02-24 13:05:28 +0100 |
| commit | a84797db94e9d242ebdf9f6feb08a63d42a14bae (patch) | |
| tree | dd4cff6ecff002121bea2872c35aa6735e716fde /plugins/btauto | |
| parent | 04d086e21cdf28c4029133a0f8fd1720d13544e8 (diff) | |
TACTIC EXTEND now takes an optional level as argument.
The syntax is: TACTIC EXTEND foo AT LEVEL i
This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.
Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:
Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
Diffstat (limited to 'plugins/btauto')
0 files changed, 0 insertions, 0 deletions