diff --git a/CHANGELOG.md b/CHANGELOG.md
index 8850914847610f140a70318f9a3afe5dbfbaa4a0..4ef9d3724fb21483d15313c1c982b0973c36b1a0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -138,6 +138,8 @@ With this release, we dropped support for Coq 8.9.
 **Changes in `heap_lang`:**
 
 * `wp_pures` now turns goals of the form `WP v {{ Φ }}` into `Φ v`.
+* Fix `wp_bind` in case of a NOP (i.e., when the given expression pattern is
+  already at the top level).
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 019a1c8af305ac3c470e1ced7c7e90d8959cf75b..6cf991f211d830d66b62e4e9b9e5b92a7962f78b 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -138,6 +138,14 @@ 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_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..39f21d758b1be6aa9a7873f715b9b89832dcb966 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -56,7 +56,7 @@ Proof. rewrite envs_entails_eq=> ->. by apply twp_value. Qed.
 Ltac wp_expr_simpl := wp_expr_eval simpl.
 
 Ltac wp_value_head :=
-  first [eapply tac_wp_value || eapply tac_twp_value].
+  first [eapply tac_wp_value | eapply tac_twp_value].
 
 Ltac wp_finish :=
   wp_expr_simpl;      (* simplify occurences of subst/fill *)
@@ -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.