From 1aec27cb24a499130ef3374402b9d2c0363a472d Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Fri, 12 Jun 2020 11:24:32 -0500
Subject: [PATCH] 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               | 12 ++++++++++++
 tests/proofmode.v                 | 19 +++++++++++++++++++
 theories/proofmode/ltac_tactics.v |  8 +++++---
 3 files changed, 36 insertions(+), 3 deletions(-)

diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index 34d52265b..fa843801d 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 af8ebb1eb..f34c1401e 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 aabad6df9..2b22211f4 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
-- 
GitLab