From 091bcc6f17d529b2c2aa6aa1529cc46452cd394a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Jan 2021 10:38:18 +0100
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 75866d8b8..e09f32e42 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -101,6 +101,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Remove the laws `pure_forall_2 : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝` from the BI
   interface and factor it into a type class `BiPureForall`.
 * Add notation `¬ P` for `P → False` to `bi_scope`.
+* Add Coq side-condition `φ` to class `ElimAcc` (similar to what we already had
+  for `ElimInv` and `ElimModal`).
 
 **Changes in `base_logic`:**
 
@@ -176,6 +178,10 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
 * Generalize HeapLang's `mapsto` (`↦`), `array` (`↦∗`), and atomic heap
   connectives to discardable fractions. See the CHANGELOG entry in the category
   `base_logic` for more information.
+* Opening an invariant or eliminating a mask-changing update modality around a
+  non-atomic weakest precondition creates an side-condition `Atomic ...`.
+  Before, this would fail with the mysterious error "iMod: cannot eliminate
+  modality (|={E1,E2}=> ...) in (WP ...)".
 
 **Changes in `heap_lang`:**
 
-- 
GitLab