From 079da034d14ad6e0c1d5f70e5f5a086fc1561f17 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 31 Oct 2018 09:45:49 +0100
Subject: [PATCH] Changelog.

---
 CHANGELOG.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6212f09f3..701c609d4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -31,6 +31,13 @@ Changes in and extensions of the theory:
   See `heap_lang/lib/increment.v` for an example.
 * [#] heap_lang now uses right-to-left evaluation order. This makes it
   significantly easier to write specifications of curried functions.
+* [#] heap_lang values are now injected in heap_lang expressions via a specific
+  constructor of the expr inductive type. This simplifies much the tactical
+  infrastructure around the language. In particular, this allow us to get rid
+  the reflexion mechanism that was needed for proving closedness, atomicity and
+  "valueness" of a term. The price to pay is the addition of new
+  "administrative" reductions in the operational semantics of the language.
+
 
 Changes in Coq:
 
@@ -85,6 +92,9 @@ Changes in Coq:
   changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
 * `wp_fork` is now written in curried form.
 * `PureExec`/`wp_pure` now supports taking multiple steps at once.
+* A new tactic, `wp_pures`, executes as many pure steps as possible, excluding
+  steps that would require unlocking subterms. Every impure wp_ tactic executes
+  this tactic before doing anything else.
 
 ## Iris 3.1.0 (released 2017-12-19)
 
-- 
GitLab