diff options
| author | Maxime Dénès | 2017-02-24 00:27:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-02-24 13:05:28 +0100 |
| commit | a84797db94e9d242ebdf9f6feb08a63d42a14bae (patch) | |
| tree | dd4cff6ecff002121bea2872c35aa6735e716fde /plugins/ltac/tacentries.mli | |
| 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/ltac/tacentries.mli')
| -rw-r--r-- | plugins/ltac/tacentries.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 969c118fb5..0695044736 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -45,7 +45,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type - to finding an argument by name (as in {!Genarg}) if there is none matching. *) -val add_ml_tactic_notation : ml_tactic_name -> +val add_ml_tactic_notation : ml_tactic_name -> level:int -> argument grammar_tactic_prod_item_expr list list -> unit (** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND ML-side macro. *) |