diff --git a/CHANGELOG.md b/CHANGELOG.md
index c4bd72c7a371683862efe5a10a6072b4082b0424..8850914847610f140a70318f9a3afe5dbfbaa4a0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -135,6 +135,10 @@ With this release, we dropped support for Coq 8.9.
   threads instead of only a single thread. The derived adequacy lemmas
   are unchanged.
 
+**Changes in `heap_lang`:**
+
+* `wp_pures` now turns goals of the form `WP v {{ Φ }}` into `Φ v`.
+
 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`).
 Note that the script is not idempotent, do not run it twice.
diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index a80047d3a7b182421acf21d45b3e77bdc26f0427..1934fcb6b2263ee40a033a85a5cf3f17e91e504d 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -60,6 +60,8 @@ Tactics to take one or more pure program steps:
   well as unary and binary arithmetic operators.
 - `wp_pures`: Perform as many pure reduction steps as possible. This
   tactic will **not** reduce lambdas/recs that are hidden behind a definition.
+  If the computation reaches a value, the `WP` will be entirely removed and the
+  postcondition becomes the new goal.
 - `wp_rec`, `wp_lam`: Perform a beta reduction.  Unlike `wp_pure`, this will
   also reduce lambdas that are hidden behind a definition.
 - `wp_let`, `wp_seq`: Reduce a let-binding or a sequential composition.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 4210930212e97c29808c1daa9edeb63f03982fdd..019a1c8af305ac3c470e1ced7c7e90d8959cf75b 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -142,6 +142,13 @@ Section tests.
     P -∗ (∀ Q Φ, Q -∗ WP e {{ Φ }}) -∗ WP e {{ _, True }}.
   Proof. iIntros "HP HW". wp_apply "HW". iExact "HP". Qed.
 
+  Lemma wp_pures_val (b : bool) :
+    ⊢ WP #b {{ _, True }}.
+  Proof. wp_pures. done. Qed.
+  Lemma twp_pures_val (b : bool) :
+    ⊢ WP #b [{ _, True }].
+  Proof. wp_pures. done. Qed.
+
   Lemma wp_cmpxchg l v :
     val_is_unboxed v →
     l ↦ v -∗ WP CmpXchg #l v v {{ _, True }}.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index d24214eb7d8e8d249014237e7ee17df51914de6c..b5a5f78ccbb117e334d9640a2bbd13fa68c820ed 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -107,8 +107,10 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
 (* TODO: do this in one go, without [repeat]. *)
 Ltac wp_pures :=
   iStartProof;
-  repeat (wp_pure _; []). (* The `;[]` makes sure that no side-condition
-                             magically spawns. *)
+  first [ (* The `;[]` makes sure that no side-condition magically spawns. *)
+          progress repeat (wp_pure _; [])
+        | wp_finish (* In case wp_pure never ran, make sure we do the usual cleanup. *)
+        ].
 
 (** Unlike [wp_pures], the tactics [wp_rec] and [wp_lam] should also reduce
 lambdas/recs that are hidden behind a definition, i.e. they should use