Verified Commit c3bfce21 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

fixup! Draft: ensure `Frame` instances are not tried before `frame_here`

parent 1b30a06d
Pipeline #50592 canceled with stage
in 51 seconds
......@@ -70,6 +70,8 @@ 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).
**Changes in `bi`:**
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment