Goal selectors are now tacticals and can be used as such.

This allows to write things like this:

    split; 2: intro _; exact I

or like this:

    eexists ?[x]; ?[x]: exact 0; trivial

This has the side-effect on making the '?' before '[x]' mandatory.

2 files changed, 17 insertions, 3 deletions

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 90a60daa6..fd71f3c42 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 9ba748e2a..dd7ad1013 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -34,8 +34,22 @@ Qed.
 
 Goal True -> True.
 Proof.
-  intros y.
+  intros y; 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.
   exact I.
-Qed.
\ No newline at end of file
+Qed.
+
+Goal True /\ (True /\ True).
+Proof.
+  dup.
+  - split; 2: (split; exact I).
+    exact I.
+  - split; 2: split; exact I.
+Qed.
+
+Goal True -> exists (x : Prop), x.
+Proof.
+  intro H; eexists ?[x]; ?[x]: exact True; assumption.
+Qed.