diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-03 10:43:24 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-14 06:21:31 +0200 |
| commit | 95a7ddee80fef2d499dce36a7e37fc5c6e374018 (patch) | |
| tree | 990b4931fe0ff1c715c93a7dfddd13f1718956cd /ltac | |
| parent | 98ed04803e022e66e17f91526ef708484fd17217 (diff) | |
Ident selectors cannot be used inside an Ltac expression.
They can still be used at the toplevel.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_ltac.ml4 | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 5f52b6711..87cc01920 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -46,6 +46,7 @@ let new_entry name = e let selector = new_entry "vernac:selector" +let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" (* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for @@ -73,7 +74,7 @@ let test_bracket_ident = GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - tactic_mode constr_may_eval constr_eval selector; + tactic_mode constr_may_eval constr_eval selector toplevel_selector; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -313,11 +314,14 @@ GEXTEND Gram ; selector: [ [ l = range_selector_or_nth; ":" -> l - | "?" ; test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id | IDENT "all" ; ":" -> SelectAll ] ] ; + toplevel_selector: + [ [ s = selector -> s + | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id ] ] + ; tactic_mode: - [ [ g = OPT selector; tac = G_vernac.subgoal_command -> tac g ] ] + [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] ; END @@ -364,7 +368,7 @@ let pr_ltac_selector = function | SelectAll -> str "all" ++ str ":" VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector -| [ selector(s) ] -> [ s ] +| [ toplevel_selector(s) ] -> [ s ] END let pr_ltac_info n = str "Info" ++ spc () ++ int n |