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

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e77fe8698..dd3f2df34 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -40,6 +40,11 @@ With this release, we dropped support for Coq 8.9.
   existentials above. As part of this change, it now uses a base name of `H` for
   pure facts rather than the previous default of `a`. This also requires some
   changes if you were implementing `FromForall`, in order to forward names.
+* Make `iFrame` "less" smart w.r.t. clean up of modalities. It now consistently
+  removes the modalities `<affine>`, `<absorbing>`, `<persistent>` and `â–¡` only
+  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.
 
 **Changes in `base_logic`:**
 
-- 
GitLab