From 2877be8a886c9d0ad8b94e43d2e46889e2b6aa3a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 29 Sep 2020 14:31:21 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd3f2df34..7aa00c58e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -45,6 +45,9 @@ With this release, we dropped support for Coq 8.9.
   if the result after framing is `True` or `emp`. In particular, it no longer
   removes `<affine>` if the result after framing is affine, and it no longer
   removes `â–¡` if the result after framing is intuitionistic.
+* 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.)
 
 **Changes in `base_logic`:**
 
-- 
GitLab