From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 test-suite/interactive/proof_block.v | 66 ++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)
 create mode 100644 test-suite/interactive/proof_block.v

(limited to 'test-suite/interactive/proof_block.v')

diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
new file mode 100644
index 00000000..31e34937
--- /dev/null
+++ b/test-suite/interactive/proof_block.v
@@ -0,0 +1,66 @@
+Goal False /\ True.
+Proof.
+split.
+  idtac.
+  idtac.
+  exact I.
+idtac.
+idtac.
+exact I.
+Qed.
+
+Lemma baz :  (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split. { eexists. split. par: trivial. }
+trivial.
+Qed.
+
+Lemma baz1 :  (True /\ False) /\ True.
+Proof.
+split. { split. par: trivial. }
+trivial.
+Qed.
+
+Lemma foo : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  { idtac.
+    unshelve eexists.
+    { apply 3. }
+    { split.
+      { idtac. trivialx. }
+      { reflexivity. } } }
+  trivial.
+Qed.
+
+Lemma foo1 : False /\ True.
+Proof.
+split.
+  { exact I. }
+  { exact I. }
+Qed.
+
+Definition banana := true + 4. 
+
+Check banana.
+
+Lemma bar : (exists n, n = 3 /\ n = 3) /\ True.
+Proof.
+split.
+  - idtac.
+    unshelve eexists.
+    + apply 3.
+    + split.
+      * idtacx. trivial. 
+      * reflexivity.
+  - trivial.
+Qed.
+
+Lemma baz2 :  ((1=0 /\ False) /\ True) /\ False.
+Proof.
+split. split. split.
+ - solve [ auto ].
+ - solve [ trivial ].
+ - solve [ trivial ].
+ - exact 6.
+Qed.
\ No newline at end of file
-- 
cgit v1.2.3