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 de474eb48c6023240217844771a0c002958cc112..6cf991f211d830d66b62e4e9b9e5b92a7962f78b 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -142,6 +142,9 @@ Section tests.
   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 }}.