From d3c20a9515cbbd57f60f7d447f649c8eba11a906 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Sun, 25 Jul 2021 19:10:45 +0200
Subject: [PATCH] Candidate changelog extension

---
 CHANGELOG.md | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 49a78c044..3843ddcd6 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`:**
 
-- 
GitLab