From f9b2155e941a8eec0d765b36330c8587bec2aca3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 26 Jun 2020 12:46:42 +0200
Subject: [PATCH] CHANGELOG

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b7958f09c..f18c74dd5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -205,6 +205,11 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Move the RAs for `nat` and `positive` and the `mnat` RA into a separate
   module. They must now be imported from `From iris.algebra Require Import
   numbers`.
+* Remove notation for 3-mask step-taking updates, and made 2-mask notation less
+  confusing by distinguishing it better from mask-changing updates.
+  Old: `|={E1,E2]â–·=> P`. New: `|={Eo}[Ei]â–·=> P`.
+  As part of this, the lemma `step_fupd_mask_mono` now also has a more
+  consistent argument order for its masks.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
-- 
GitLab