Skip to content
Snippets Groups Projects
Verified Commit d3c20a95 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

Candidate changelog extension

parent 20789d80
No related branches found
No related tags found
No related merge requests found
......@@ -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`:**
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment