diff --git a/CHANGELOG.md b/CHANGELOG.md index e09f32e42acf6302dbfc8cd38f62d6c9de4bef97..835085e1cb9171f519531c144752ca385c889f1c 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`:**