From f7c9e03e97eaa787e56ba351df68e8109d0b608b Mon Sep 17 00:00:00 2001 From: Ike Mulder <i.mulder@cs.ru.nl> Date: Tue, 5 Mar 2024 15:49:07 +0000 Subject: [PATCH] Fix very wide lines in CHANGELOG --- CHANGELOG.md | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f3d7e0479..3b4e284c3 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -70,7 +70,11 @@ lemma. Local Instance frame_exist_instantiate_disabled : FrameInstantiateExistDisabled := {}. ``` - `iFrame` will not instantiate existential quantifiers below connectives such as `-∗`, `∀`, `→` and `WP`, since this is more frequently unsafe (MR: iris/iris!1035). If you have custom recursive `Frame` instances for which you want to disable instantiating existential quantifiers, you need to replace the `Frame ...` premise of your instance with `(FrameInstantiateExistDisabled → Frame ...)`. + `iFrame` will not instantiate existential quantifiers below connectives such as + `-∗`, `∀`, `→` and `WP`, since this is more frequently unsafe (MR: iris/iris!1035). + If you have custom recursive `Frame` instances for which you want to disable + instantiating existential quantifiers, you need to replace the `Frame ...` premise + of your instance with `(FrameInstantiateExistDisabled → Frame ...)`. **Changes in `base_logic`:** -- GitLab