From 42943c18f694197302cb4c091c65957f78171349 Mon Sep 17 00:00:00 2001
From: Robbert <gitlab-sws@robbertkrebbers.nl>
Date: Thu, 7 Jan 2021 09:38:52 +0100
Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s)
---
CHANGELOG.md | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index e09f32e42..835085e1c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -179,8 +179,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
connectives to discardable fractions. See the CHANGELOG entry in the category
`base_logic` for more information.
* Opening an invariant or eliminating a mask-changing update modality around a
- non-atomic weakest precondition creates an side-condition `Atomic ...`.
- Before, this would fail with the mysterious error "iMod: cannot eliminate
+ non-atomic weakest precondition creates a side-condition `Atomic ...`.
+ Before, this would fail with the unspecific error "iMod: cannot eliminate
modality (|={E1,E2}=> ...) in (WP ...)".
**Changes in `heap_lang`:**
--
GitLab