Commit 3d1cf0c2 authored by Ralf Jung's avatar Ralf Jung Committed by Robbert Krebbers
Browse files

add changelog

parent d1d214ab
......@@ -81,6 +81,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
and either affine or absorbing.
* Fix the statement of the lemma `fupd_plainly_laterN`; the old lemma was a
duplicate of `fupd_plain_laterN`.
* Strengthen `big_sepL2_app_inv` by weakening a premise (it is sufficient for
one of the two pairs of lists to have equal length).
**Changes in `proofmode`:**
......
Supports Markdown
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