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 | |
| 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')
| -rw-r--r-- | plugins/ltac/tacentries.ml | 12 | ||||
| -rw-r--r-- | plugins/ltac/tacentries.mli | 2 |
2 files changed, 8 insertions, 6 deletions
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 2e2b55be74..8570b5a447 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -302,9 +302,9 @@ let cons_production_parameter = function | TacTerm _ -> None | TacNonTerm (_, _, id) -> Some id -let add_glob_tactic_notation local n prods forml ids tac = +let add_glob_tactic_notation local ~level prods forml ids tac = let parule = { - tacgram_level = n; + tacgram_level = level; tacgram_prods = prods; } in let tacobj = { @@ -360,7 +360,7 @@ let extend_atomic_tactic name entries = in List.iteri add_atomic entries -let add_ml_tactic_notation name prods = +let add_ml_tactic_notation name ~level prods = let len = List.length prods in let iter i prods = let open Tacexpr in @@ -372,10 +372,12 @@ let add_ml_tactic_notation name prods = let entry = { mltac_name = name; mltac_index = len - i - 1 } in let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in let tac = TacML (Loc.ghost, entry, List.map map ids) in - add_glob_tactic_notation false 0 prods true ids tac + add_glob_tactic_notation false ~level prods true ids tac in List.iteri iter (List.rev prods); - extend_atomic_tactic name prods + (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at + tactic_expr level 0) *) + if Int.equal level 0 then extend_atomic_tactic name prods (**********************************************************************) (** Ltac quotations *) 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. *) |