From b958d569a1613c673ff52be14661b298a56b71fc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 20 Sep 2019 09:11:46 +0200
Subject: [PATCH] test output of iStopProof

---
 tests/proofmode.ref | 19 +++++++++++++++++++
 tests/proofmode.v   |  3 ++-
 2 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 03b2e892b..51b84fa27 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -21,6 +21,25 @@
   --------------------------------------â–¡
   Q ∨ P
   
+"test_iStopProof"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  ============================
+  "H1" : emp
+  --------------------------------------â–¡
+  "H2" : Q
+  --------------------------------------∗
+  Q
+  
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  ============================
+  □ emp ∗ Q -∗ Q
 "test_iDestruct_and_emp"
      : string
 1 subgoal
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8e52115fd..adfc17780 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -44,8 +44,9 @@ Definition bar : PROP := (∀ P, foo P)%I.
 Lemma test_unfold_constants : bar.
 Proof. iIntros (P) "HP //". Qed.
 
+Check "test_iStopProof".
 Lemma test_iStopProof Q : emp -∗ Q -∗ Q.
-Proof. iIntros "#H1 H2". iStopProof. by rewrite bi.sep_elim_r. Qed.
+Proof. iIntros "#H1 H2". Show. iStopProof. Show. 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)).
-- 
GitLab