diff options
| author | Maxime Dénès | 2016-09-28 15:28:51 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-28 15:28:51 +0200 |
| commit | 2c4f3c2bcf93d023b53a9f2ec6b151d4df696c84 (patch) | |
| tree | 2a8f3c92e40efe0eb5651c01bd3bf613bd68cf2c /ltac | |
| parent | 72c1fefcfb3f0dff02005034685f6b58ff84b3cc (diff) | |
| parent | 4b61c0693d453dd0026792185354d68ba1db9022 (diff) | |
Merge remote-tracking branch 'github/pr/232' into v8.6
Was PR#232: Fix the parsing of goal selectors.
Diffstat (limited to 'ltac')
| -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 9f2c0a93e7..a3ca4ebc4a 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -45,7 +45,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" @@ -79,7 +78,7 @@ let warn_deprecated_appcontext = GEXTEND Gram GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg - tactic_mode constr_may_eval constr_eval selector toplevel_selector; + tactic_mode constr_may_eval constr_eval toplevel_selector; tactic_then_last: [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> @@ -316,13 +315,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 ] ] |