diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index c74421133253dfec690def68200321cf7d801e5c..ab4d717041fb158023d6ea3fae514d4a752457a1 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 0e1632838da9351acc3a7be9a4aedc8a2f86aa92..64e37382064e716331fc28ad29f4b1d9f4bea613 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 2e6e82782112fac46036d29e37624c6aaa200931..4fd2570e8f5650c82e2aacbdfad9ff0f10c5629b 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.