diff --git a/CHANGELOG.md b/CHANGELOG.md index dd3f2df34329287fe236e27d997906dbec88769d..7aa00c58e5967e5f8d25214ebf8eaf9c8a941f25 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`:**