From 0f2b25d8b89a5ef3f3824b1840d97dd79a287d0e Mon Sep 17 00:00:00 2001
From: Cyprien Mangin
Date: Wed, 24 Jun 2015 11:12:19 +0200
Subject: Add test-suite file for goal selectors.

---
 test-suite/success/goal_selector.v | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 test-suite/success/goal_selector.v

diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
new file mode 100644
index 0000000000..fc3c8a92db
--- /dev/null
+++ b/test-suite/success/goal_selector.v
@@ -0,0 +1,33 @@
+Inductive two : bool -> Prop :=
+| Zero : two false
+| One : two true.
+
+Ltac dup :=
+  let H := fresh in assert (forall (P : Prop), P -> P -> P) as H by (intros; trivial);
+  apply H; clear H.
+
+Lemma transform : two false <-> two true.
+Proof. split; intros _; constructor. Qed.
+
+Goal two false /\ two true /\ two false /\ two true /\ two true /\ two true.
+Proof.
+  do 2 dup.
+  - repeat split.
+    [2, 4-99, 100-3]:idtac.
+    [2-5]:exact One.
+    par:exact Zero.
+  - repeat split.
+    [3-6]:swap 1 4.
+    [1-5]:swap 1 5.
+    [0-4]:exact One.
+    all:exact Zero.
+  - repeat split.
+    [1, 3]:exact Zero.
+    [1, 2, 3, 4]: exact One.
+  - repeat split.
+    all:apply transform.
+    [2, 4, 6]:apply transform.
+    all:apply transform.
+    [1-5]:apply transform.
+    [1-6]:exact One.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3