fix wp_bind with empty context

tests/heap_lang.v

@@ -138,6 +138,11 @@ Section tests.
     by replace (S n - 1)%Z with (n:Z) by lia.
   Qed.
 
+  (* Make sure [wp_bind] works even when it changes nothing. *)
+  Lemma wp_bind_nop (e : expr) :
+    ⊢ WP e + #0 {{ _, True }}.
+  Proof. wp_bind (e + #0)%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.

theories/heap_lang/proofmode.v

@@ -167,11 +167,11 @@ Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
-    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
-    || fail "wp_bind: cannot find" efoc "in" e
+    first [ reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
+          | fail "wp_bind: cannot find" efoc "in" e ]
   | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
-    reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
-    || fail "wp_bind: cannot find" efoc "in" e
+    first [ reshape_expr e ltac:(fun K e' => unify e' efoc; twp_bind_core K)
+          | fail "wp_bind: cannot find" efoc "in" e ]
   | _ => fail "wp_bind: not a 'wp'"
   end.