diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index c535692a0c17919272a573fce5a3f7e9b0fd4d53..bc516583777a44832c6981234a3ae9faab51e3b5 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 197fed735db30bd25ed9297b007774f832c288d7..be7245aedd0cf24f87a8d14012044921c9b51870 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.