From 1b93cb011951534ee8560c3a6fd5c410ce98208e Mon Sep 17 00:00:00 2001
From: Tej Chajed <tchajed@mit.edu>
Date: Tue, 2 Feb 2021 09:24:24 -0600
Subject: [PATCH] Fix wp_bind's error message

Fixes #401
---
 iris_heap_lang/proofmode.v | 4 ++--
 tests/heap_lang.ref        | 6 ++++++
 tests/heap_lang.v          | 6 ++++++
 3 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index c74421133..ab4d71704 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -197,10 +197,10 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
     first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
-          | fail "wp_bind: cannot find" efoc "in" e ]
+          | fail 1 "wp_bind: cannot find" efoc "in" e ]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
     first [ reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
-          | fail "wp_bind: cannot find" efoc "in" e ]
+          | fail 1 "wp_bind: cannot find" efoc "in" e ]
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
diff --git a/tests/heap_lang.ref b/tests/heap_lang.ref
index 0e1632838..64e373820 100644
--- a/tests/heap_lang.ref
+++ b/tests/heap_lang.ref
@@ -88,6 +88,12 @@ Tactic failure: wp_store: cannot find 'Store' in (Fork #()).
      : string
 The command has indeed failed with message:
 Tactic failure: wp_store: cannot find l ↦ ?.
+"(t)wp_bind_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
+The command has indeed failed with message:
+Tactic failure: wp_bind: cannot find (! ?e)%E in (Val #()).
 1 goal
   
   Σ : gFunctors
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 2e6e82782..4fd2570e8 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -173,6 +173,12 @@ Section tests.
     ⊢ WP #l <- #0 {{ _, True }}.
   Proof. Fail wp_store. Abort.
 
+  Check "(t)wp_bind_fail".
+  Lemma wp_bind_fail : ⊢ WP #() {{ v, True }}.
+  Proof. Fail wp_bind (!_)%E. Abort.
+  Lemma twp_bind_fail : ⊢ WP #() [{ v, True }].
+  Proof. Fail wp_bind (!_)%E. Abort.
+
   Lemma wp_apply_evar e P :
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
-- 
GitLab