diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 019a1c8af305ac3c470e1ced7c7e90d8959cf75b..de474eb48c6023240217844771a0c002958cc112 100644
--- a/tests/heap_lang.v
+++ b/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.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index b5a5f78ccbb117e334d9640a2bbd13fa68c820ed..48448b35801d1330b185530d4198f55e42961573 100644
--- a/theories/heap_lang/proofmode.v
+++ b/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.