From 98ed04803e022e66e17f91526ef708484fd17217 Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Fri, 3 Jun 2016 10:24:36 +0200
Subject: 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.
---
 test-suite/success/destruct.v      |  2 +-
 test-suite/success/goal_selector.v | 18 ++++++++++++++++--
 2 files changed, 17 insertions(+), 3 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 90a60daa66..fd71f3c423 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 9ba748e2a5..dd7ad10131 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.
-- 
cgit v1.2.3