Update changlog.

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.

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) := {