From 821937aee71bf9439158e27e06f7b4f74289b209 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 23 May 2016 16:57:31 +0200
Subject: STM: proof block detection made optional + simple test

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

(limited to 'test-suite')

diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
new file mode 100644
index 0000000000..ff920b671e
--- /dev/null
+++ b/test-suite/interactive/proof_block.v
@@ -0,0 +1,56 @@
+
+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


From e4d66a03148243f7611f4d7c164e775877184e03 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 6 Jun 2016 05:50:07 -0400
Subject: Error box detection run only on error

Advantage: 0 cost if no error occurs
Disadvantage: a box *must* end with the error absorbing command
---
 test-suite/interactive/proof_block.v | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
index ff920b671e..31e3493768 100644
--- a/test-suite/interactive/proof_block.v
+++ b/test-suite/interactive/proof_block.v
@@ -1,3 +1,13 @@
+Goal False /\ True.
+Proof.
+split.
+  idtac.
+  idtac.
+  exact I.
+idtac.
+idtac.
+exact I.
+Qed.
 
 Lemma baz :  (exists n, n = 3 /\ n = 3) /\ True.
 Proof.
@@ -26,7 +36,7 @@ Qed.
 Lemma foo1 : False /\ True.
 Proof.
 split.
-  exact I.
+  { exact I. }
   { exact I. }
 Qed.
 
-- 
cgit v1.2.3