diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 08:32:54 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-17 08:32:54 +0100 |
| commit | f2bbdd31a6aa62d8a000f5a91f666e68e7241964 (patch) | |
| tree | 1f4192575cdde8e8f09063671c1e420884fc58e7 /plugins/ltac | |
| parent | dae19c34325b2b98ee0a45ac7908a0c28021ba9e (diff) | |
| parent | a84797db94e9d242ebdf9f6feb08a63d42a14bae (diff) | |
Merge PR#445: TACTIC EXTEND now takes an optional level as argument.
Diffstat (limited to 'plugins/ltac')
| -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 75edf150e..cd8c9e471 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 969c118fb..069504473 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. *) |