From 0e22868626e602610a006bee362cafce7ef866ef Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 10 Nov 2020 10:08:54 +0100
Subject: [PATCH] add docs and changelog entry

---
 CHANGELOG.md      | 4 ++++
 docs/heap_lang.md | 2 ++
 2 files changed, 6 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index c4bd72c7a..885091484 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 a80047d3a..1934fcb6b 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.
-- 
GitLab