Fix wp_bind's error message

Fixes #401

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.
 

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

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.