diff --git a/CHANGELOG.md b/CHANGELOG.md index 49a78c044ea4cc1c4e3ea333562ff144643627c4..3843ddcd6562c25a1c6b406bf087fd58a3c615a9 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -74,8 +74,13 @@ Coq 8.11 is no longer supported in this version of Iris. * `iMod`/`iModIntro` show proper error messages when they fail due to mask mismatches. To support this, the proofmode typeclass `FromModal` now takes an additional pure precondition. -* Fix performance of `iFrame` in logics without `BiAffine`. (by Paolo G. - Giarrusso, BedRock Systems) +* Fix performance of `iFrame` in logics without `BiAffine`. + To adjust your code if you use such logics and define `Frame` instances, + ensure these instances to have priority at least 2: they should have either at + least 2 (non-dependent) premises, or an explicit priority. + References: docs for `frame_here_absorbing` and + https://coq.inria.fr/refman/addendum/type-classes.html#coq:cmd.Instance. (by + Paolo G. Giarrusso, BedRock Systems) **Changes in `bi`:**