From d38ec11eecfa0b6e2c3882cb45b5f7da010584c8 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Sun, 16 Jan 2022 21:04:01 -0500 Subject: [PATCH] changelog --- CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 57a15c2fb..3b11bdd14 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -38,6 +38,10 @@ lemma. Proofs that are generic in `PROP` might have to add those new classes as assumptions to remain compatible, and code that instantiates the BI interface needs to provide instances for the new classes. +* Make `frame_fractional` not an instance any more; instead fractional + propositions that want to support framing are expected to register an + appropriate instance themselves. HeapLang and gen_heap `↦` still support + framing, but the other fractional propositions in Iris do not. **Changes in `heap_lang`:** -- GitLab