diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 03b2e892b40437d5f80081bb0a87c7bb56d4bd09..51b84fa2780eb1656983403b535c8672e80e4708 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 8e52115fd7da796277b199fd5ad24a4a87f54fd1..adfc177806e26664ff802370167e7eb40a3d4001 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)).