diff options
| -rw-r--r-- | ltac/g_ltac.ml4 | 12 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 2 | ||||
| -rw-r--r-- | test-suite/success/goal_selector.v | 2 |
3 files changed, 10 insertions, 6 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 diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index fd71f3c42..90a60daa6 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -106,7 +106,7 @@ Goal exists x, S 0 = S x. eexists ?[x]. destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S ?x). -?[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) +[x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v index dd7ad1013..91fb54d9a 100644 --- a/test-suite/success/goal_selector.v +++ b/test-suite/success/goal_selector.v @@ -51,5 +51,5 @@ Qed. Goal True -> exists (x : Prop), x. Proof. - intro H; eexists ?[x]; ?[x]: exact True; assumption. + intro H; eexists ?[x]. [x]: exact True. 1: assumption. Qed. |