From 672f4a53a82cf93ebf761582b261c62565ab7c75 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 13:29:41 +0100
Subject: [PATCH] changelog, TWP test

---
 CHANGELOG.md      | 2 ++
 tests/heap_lang.v | 3 +++
 2 files changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 885091484..4ef9d3724 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 de474eb48..6cf991f21 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 }}.
-- 
GitLab