From cfb8421aa64ee993f68f47bbe404e3aecff54f08 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 13 Jun 2018 11:00:24 +0200
Subject: [PATCH] Update changlog.

---
 CHANGELOG.md          | 4 ++++
 theories/bi/updates.v | 2 --
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index bcf5ff865..5e41ab481 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 Changes in and extensions of the theory:
 
+* [#] Change in the definition of WP, so that there is a fancy update between
+  the quantification over the next states and the later modality. This makes it
+  possible to prove more powerful lifting lemmas: The new versions feature an
+  "update that take a step".
 * [#] Add weakest preconditions for total program correctness.
 * [#] "(Potentially) stuck" weakest preconditions are no longer considered
   experimental.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 75aa5770e..1e63f5b73 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -32,8 +32,6 @@ Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_s
 Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I : bi_scope.
 Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
 
-
-
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
 Record BiBUpdMixin (PROP : bi) `(BUpd PROP) := {
-- 
GitLab