diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 57992ccc987e921af097c8a1edf82395f3d2dc73..9db702ed664dbb6e7b26b154098a31bd41accde3 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -178,6 +178,50 @@ Tactic failure: iSpecialize: Q not persistent.
   ⌜φ⌝
 1 goal
   
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  ⌜φ⌝
+"test_iSpecialize_impl_pure"
+     : string
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  <affine> ⌜φ⌝
+1 goal
+  
+  PROP : bi
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  "H1" : P
+  --------------------------------------â–¡
+  <affine> ⌜φ⌝
+"test_iSpecialize_impl_pure_affine"
+     : string
+1 goal
+  
+  PROP : bi
+  BiAffine0 : BiAffine PROP
+  φ : Prop
+  P, Q : PROP
+  H : φ
+  ============================
+  --------------------------------------∗
+  ⌜φ⌝
+1 goal
+  
   PROP : bi
   BiAffine0 : BiAffine PROP
   φ : Prop
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 8a48e493082f95eac582370e3ae983630b69a3a7..700bb4382f4f29d49b28d6db96acfec96952bfc7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -480,6 +480,38 @@ Restart.
   by iFrame.
 Abort.
 
+Check "test_iSpecialize_impl_pure".
+Lemma test_iSpecialize_forall_pure (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Adds an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
+Check "test_iSpecialize_impl_pure_affine".
+Lemma test_iSpecialize_forall_pure_affine `{!BiAffine PROP} (φ : Prop) P Q :
+  φ → □ (∀ _ : φ, P) -∗ (∀ _ : φ, Q) -∗ P ∗ Q.
+Proof.
+  iIntros (?) "#H1 H2".
+  (* Does not add an affine modality *)
+  iSpecialize ("H1" with "[]"). { Show. done. }
+  iSpecialize ("H2" with "[]"). { Show. done. }
+Restart.
+  iIntros (?) "#H1 H2".
+  (* Solving it directly as a pure goal also works. *)
+  iSpecialize ("H1" with "[% //]").
+  iSpecialize ("H2" with "[% //]").
+  by iFrame.
+Abort.
+
 Check "test_iAssert_intuitionistic".
 Lemma test_iAssert_intuitionistic `{!BiBUpd PROP} P :
   □ P -∗ □ |==> P.