Skip to content
Snippets Groups Projects
Commit 42943c18 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Robbert Krebbers
Browse files

Apply 2 suggestion(s) to 1 file(s)

parent 091bcc6f
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
CHANGELOG.md
+ 2
− 2
View file @ 42943c18
...@@ -179,8 +179,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`. ...@@ -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 connectives to discardable fractions. See the CHANGELOG entry in the category
`base_logic` for more information. `base_logic` for more information.
* Opening an invariant or eliminating a mask-changing update modality around a * Opening an invariant or eliminating a mask-changing update modality around a
non-atomic weakest precondition creates an side-condition `Atomic ...`. non-atomic weakest precondition creates a side-condition `Atomic ...`.
Before, this would fail with the mysterious error "iMod: cannot eliminate Before, this would fail with the unspecific error "iMod: cannot eliminate
modality (|={E1,E2}=> ...) in (WP ...)". modality (|={E1,E2}=> ...) in (WP ...)".
**Changes in `heap_lang`:** **Changes in `heap_lang`:**
......
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