diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 93b90699c55e66edf9d87d38478d714bf882be8d..be894c20a79851c59c2fd6be4b9de8ebab79c358 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -54,6 +54,29 @@
   --------------------------------------â–¡
   <affine> (P ∗ Q)
   
+"test_iDestruct_spatial"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  ============================
+  "HQ" : <affine> Q
+  --------------------------------------∗
+  Q
+  
+"test_iDestruct_spatial_affine"
+     : string
+1 subgoal
+  
+  PROP : sbi
+  Q : PROP
+  Affine0 : Affine Q
+  ============================
+  "HQ" : Q
+  --------------------------------------∗
+  Q
+  
 The command has indeed failed with message:
 Ltac call to "done" failed.
 No applicable tactic.
diff --git a/tests/proofmode.v b/tests/proofmode.v
index b41edc481b33abee85bdff9663bdd11f1b8e4021..fc1e7df41d68ad0bb4bdb3f38cf5f4ca9d082344 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -90,6 +90,21 @@ Lemma test_iDestruct_intuitionistic_affine_bi `{!BiAffine PROP} P Q `{!Persisten
   Q ∗ (Q -∗ P) -∗ P ∗ Q.
 Proof. iIntros "[HQ HQP]". iDestruct ("HQP" with "HQ") as "#HP". by iFrame. Qed.
 
+Check "test_iDestruct_spatial".
+Lemma test_iDestruct_spatial Q : □ Q -∗ Q.
+Proof. iIntros "#HQ". iDestruct "HQ" as "-#HQ". Show. done. Qed.
+
+Check "test_iDestruct_spatial_affine".
+Lemma test_iDestruct_spatial_affine Q `{!Affine Q} : □ Q -∗ Q.
+Proof.
+  iIntros "#-#HQ".
+  (* Since [Q] is affine, it should not add an <affine> modality *)
+  Show. done.
+Qed.
+
+Lemma test_iDestruct_spatial_noop Q : Q -∗ Q.
+Proof. iIntros "-#HQ". done. Qed.
+
 Lemma test_iIntros_pure (ψ φ : Prop) P : ψ → (⌜ φ ⌝ → P → ⌜ φ ∧ ψ ⌝ ∧ P)%I.
 Proof. iIntros (??) "H". auto. Qed.