From 09332c3793c8ee2b2c6be9a83192cd231662959d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 2 Nov 2020 11:20:22 +0100
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e2dfa3d07..e6ec13436 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -80,7 +80,7 @@ With this release, we dropped support for Coq 8.9.
   interface and factor it into a type class `BiPureForall`.
 * Add notation `¬ P` for `P → False` to `bi_scope`.
 
-**Changes in `base_logic`:**
+**Changes in the logic (`base_logic`, `bi`):**
 
 * Add a `ghost_var` library that provides (fractional) ownership of a ghost
   variable of arbitrary `Type`.
@@ -110,6 +110,8 @@ With this release, we dropped support for Coq 8.9.
 * Add an `mnat` library on top of `mnat_auth` that supports ghost state which is
   an authoritative, monotonically-increasing `nat` with a proposition giving a
   persistent lower bound. See `base_logic.lib.mnat` for further details.
+* Add big op lemmas `big_op{L,L2,M,M2,S}_intuitionistically_forall` and
+  `big_sepL2_forall`, `big_sepMS_forall`, `big_sepMS_impl`, and `big_sepMS_dup`.
 
 **Changes in `program_logic`:**
 
-- 
GitLab