From e4d66a03148243f7611f4d7c164e775877184e03 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
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/interactive')

diff --git a/test-suite/interactive/proof_block.v b/test-suite/interactive/proof_block.v
index ff920b671..31e349376 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