Goal selectors now use the keyword [only].

This fixes some parsing problems when doing things like
[let n := 2 in idtac n]. See bug #4877.

3 files changed, 24 insertions, 10 deletions

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index b5494a7cbb..fbeb89a634 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 ] ]
diff --git a/test-suite/bugs/closed/4877.v b/test-suite/bugs/closed/4877.v
new file mode 100644
index 0000000000..7e3c78dc2e
--- /dev/null
+++ b/test-suite/bugs/closed/4877.v
@@ -0,0 +1,12 @@
+Ltac induction_last :=
+  let v := match goal with
+           | |- forall x y, _ = _ -> _ => 1
+           | |- forall x y, _ -> _ = _ -> _ => 2
+           | |- forall x y, _ -> _ -> _ = _ -> _ => 3
+           end in
+  induction v.
+
+Goal forall n m : nat, True -> n = m -> m = n.
+  induction_last.
+  reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 91fb54d9a1..8681405175 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -34,7 +34,7 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y; 1-2 : repeat idtac.
+  intros y; only 1-2 : repeat idtac.
   1-1:match goal with y : _ |- _ => let x := y in idtac x end.
   Fail 1-1:let x := y in idtac x.
   1:let x := y in idtac x.
@@ -44,12 +44,12 @@ Qed.
 Goal True /\ (True /\ True).
 Proof.
   dup.
-  - split; 2: (split; exact I).
+  - split; only 2: (split; exact I).
     exact I.
-  - split; 2: split; exact I.
+  - split; only 2: split; exact I.
 Qed.
 
 Goal True -> exists (x : Prop), x.
 Proof.
-  intro H; eexists ?[x]. [x]: exact True. 1: assumption.
+  intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
 Qed.