From 2c2565acfcc3a18424a63cb1ffd84d0a76be3d9e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 1 Oct 2020 09:49:17 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2b8c78888..9ea980134 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -48,6 +48,9 @@ With this release, we dropped support for Coq 8.9.
 * Allow framing below an `<affine>` modality if the hypothesis that is framed is
   affine. (Previously, framing below `<affine>` was only possible if the
   hypothesis that is framed resides in the intuitionistic context.)
+* 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`.
 
 **Changes in `base_logic`:**
 
-- 
GitLab