From 8f319109110153d6282f0f040d481dca75885d35 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 3 Jun 2018 13:44:56 +0200
Subject: [PATCH] add an interesting test output

---
 tests/proofmode.ref | 12 ++++++++++++
 tests/proofmode.v   |  2 +-
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index c535692a0..bc5165837 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -19,3 +19,15 @@
   --------------------------------------â–¡
   Q ∨ P
   
+1 subgoal
+  
+  PROP : sbi
+  P, Q : PROP
+  Persistent0 : Persistent P
+  Persistent1 : Persistent Q
+  ============================
+  _ : P
+  _ : Q
+  --------------------------------------â–¡
+  <affine> (P ∗ Q)
+  
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 197fed735..be7245aed 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -54,7 +54,7 @@ Qed.
 
 Lemma test_iDestruct_and_emp P Q `{!Persistent P, !Persistent Q} :
   P ∧ emp -∗ emp ∧ Q -∗ <affine> (P ∗ Q).
-Proof. iIntros "[#? _] [_ #?]". auto. Qed.
+Proof. iIntros "[#? _] [_ #?]". Show. auto. Qed.
 
 Lemma test_iIntros_persistent P Q `{!Persistent Q} : (P → Q → P ∧ Q)%I.
 Proof. iIntros "H1 #H2". by iFrame "∗#". Qed.
-- 
GitLab