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