diff options
author | 2017-03-17 08:32:54 +0100 | |
---|---|---|
committer | 2017-03-17 08:32:54 +0100 | |
commit | f2bbdd31a6aa62d8a000f5a91f666e68e7241964 (patch) | |
tree | 1f4192575cdde8e8f09063671c1e420884fc58e7 /plugins/ltac/tacentries.ml | |
parent | dae19c34325b2b98ee0a45ac7908a0c28021ba9e (diff) | |
parent | a84797db94e9d242ebdf9f6feb08a63d42a14bae (diff) |
Merge PR#445: TACTIC EXTEND now takes an optional level as argument.
Diffstat (limited to 'plugins/ltac/tacentries.ml')
-rw-r--r-- | plugins/ltac/tacentries.ml | 12 |
1 files changed, 7 insertions, 5 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 *) |