diff options
Diffstat (limited to 'ltac/g_ltac.ml4')
| -rw-r--r-- | ltac/g_ltac.ml4 | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index d128b4d08..54229bb2a 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -48,7 +48,6 @@ let new_entry name = let e = Gram.entry_create name in e -let selector = new_entry "vernac:selector" let toplevel_selector = new_entry "vernac:toplevel_selector" let tacdef_body = new_entry "tactic:tacdef_body" @@ -84,7 +83,7 @@ let warn_deprecated_appcontext = GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint - tactic_mode constr_may_eval constr_eval selector toplevel_selector + tactic_mode constr_may_eval constr_eval toplevel_selector operconstr; tactic_then_last: @@ -322,13 +321,16 @@ GEXTEND Gram l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] ; + selector_body: + [ [ l = range_selector_or_nth -> l + | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ] + ; selector: - [ [ l = range_selector_or_nth; ":" -> l - | IDENT "all" ; ":" -> SelectAll ] ] + [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] ; toplevel_selector: - [ [ s = selector -> s - | test_bracket_ident; "["; id = ident; "]"; ":" -> SelectId id ] ] + [ [ sel = selector_body; ":" -> sel + | IDENT "all"; ":" -> SelectAll ] ] ; tactic_mode: [ [ g = OPT toplevel_selector; tac = G_vernac.subgoal_command -> tac g ] ] |