diff --git a/CHANGELOG.md b/CHANGELOG.md
index bcf5ff865d0172c8e00b7de3cf4bce6c3e134d8b..5e41ab481e89ceaf60c45578b753a9de009d818e 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 75aa5770ec2aa423ce12866dab193fa42af52f55..1e63f5b738c57e69b7953a9a49545f47137c8a9f 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) := {