Fix error message when with [% //] fails

Fixes #325.

Also added a tests for the various `iSpecialize` error cases involving
the `[%]` and `[//]` specialization patterns.

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"

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.

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