diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 34d52265be0f8d05e97247815472e27f21d3c97b..fa843801d94788852473772ecd007a6f30868634 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -94,6 +94,18 @@ The command has indeed failed with message:
 Tactic failure: iElaborateSelPat: "HQ" not found.
 The command has indeed failed with message:
 Tactic failure: iElaborateSelPat: "HQ" not found.
+"test_iSpecialize_pure_error"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpecialize: P not pure.
+"test_iSpecialize_pure_error"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpecialize: cannot solve φ using done.
+"test_iSpecialize_done_error"
+     : string
+The command has indeed failed with message:
+Tactic failure: iSpecialize: cannot solve P using done.
 The command has indeed failed with message:
 Tactic failure: iSpecialize: Q not persistent.
 "test_iAssert_intuitionistic"
diff --git a/tests/proofmode.v b/tests/proofmode.v
index af8ebb1eb1ee11ab1c003843fad0f8e9be0e6bb0..f34c1401e3b0423f832cd7967581ea1fe7fbd140 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -184,6 +184,25 @@ Lemma test_iSpecialize_pure (φ : Prop) Q R :
   φ → (⌜φ⌝ -∗ Q) → ⊢ Q.
 Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
 
+Lemma test_iSpecialize_pure_done (φ: Prop) Q :
+  φ → (⌜φ⌝ -∗ Q) ⊢ Q.
+Proof. iIntros (HP) "HQ". iApply ("HQ" with "[% //]"). Qed.
+
+Check "test_iSpecialize_pure_error".
+Lemma test_iSpecialize_not_pure_error P Q :
+  (P -∗ Q) ⊢ Q.
+Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[%]"). Abort.
+
+Check "test_iSpecialize_pure_error".
+Lemma test_iSpecialize_pure_done_error (φ: Prop) Q :
+  (⌜φ⌝ -∗ Q) ⊢ Q.
+Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[% //]"). Abort.
+
+Check "test_iSpecialize_done_error".
+Lemma test_iSpecialize_done_error P Q :
+  (P -∗ Q) ⊢ Q.
+Proof. iIntros "HQ". Fail iSpecialize ("HQ" with "[//]"). Abort.
+
 Lemma test_iSpecialize_Coq_entailment P Q R :
   (⊢ P) → (P -∗ Q) → (⊢ Q).
 Proof. iIntros (HP HPQ). iDestruct (HPQ $! HP) as "?". done. Qed.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index aabad6df9cb8e5d9855c08c923165196043f1dba..2b22211f4ae89c090954c9c1f9e37e73e2bcda33 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -845,9 +845,11 @@ Ltac iSpecializePat_go H1 pats :=
   let solve_done d :=
     lazymatch d with
     | true =>
-       done ||
-       let Q := match goal with |- envs_entails _ ?Q => Q end in
-       fail "iSpecialize: cannot solve" Q "using done"
+       first [ done
+             | let Q := match goal with |- envs_entails _ ?Q => Q end in
+               fail 1 "iSpecialize: cannot solve" Q "using done"
+             | let Q := match goal with |- ?Q => Q end in
+               fail 1 "iSpecialize: cannot solve" Q "using done" ]
     | false => idtac
     end in
   let Δ := iGetCtx in