From aa7871c78035e3b23650f40291096293b5a4b50b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Sep 2019 14:40:34 +0200
Subject: [PATCH] Test cases for iStopProof.

---
 tests/proofmode.ref | 5 +++++
 tests/proofmode.v   | 7 +++++++
 2 files changed, 12 insertions(+)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 005c8279b..03b2e892b 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -433,6 +433,11 @@ Tactic failure: iFrame: cannot frame Q.
   ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
              ={E1,E2}=∗ QQQQQQQQQQQQQQQQQQ ∗ QQQQQQQQQQQQQQQQQQ
   
+"iStopProof_not_proofmode"
+     : string
+The command has indeed failed with message:
+Ltac call to "iStopProof" failed.
+Tactic failure: iStopProof: proofmode not started.
 "iAlways_spatial_non_empty"
      : string
 The command has indeed failed with message:
diff --git a/tests/proofmode.v b/tests/proofmode.v
index e9c431fea..8e52115fd 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -44,6 +44,9 @@ Definition bar : PROP := (∀ P, foo P)%I.
 Lemma test_unfold_constants : bar.
 Proof. iIntros (P) "HP //". Qed.
 
+Lemma test_iStopProof Q : emp -∗ Q -∗ Q.
+Proof. iIntros "#H1 H2". iStopProof. by rewrite bi.sep_elim_r. Qed.
+
 Lemma test_iRewrite {A : ofeT} (x y : A) P :
   □ (∀ z, P -∗ <affine> (z ≡ y)) -∗ (P -∗ P ∧ (x,x) ≡ (y,x)).
 Proof.
@@ -765,6 +768,10 @@ Section error_tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
+Check "iStopProof_not_proofmode".
+Lemma iStopProof_not_proofmode : 10 = 10.
+Proof. Fail iStopProof. Abort.
+
 Check "iAlways_spatial_non_empty".
 Lemma iAlways_spatial_non_empty P :
   P -∗ □ emp.
-- 
GitLab