Commit cccaa011 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files


parent 2532b236
......@@ -73,6 +73,8 @@ HeapLang, which is now in a separate package `coq-iris-heap-lang`.
been working properly for quite some time).
* Strengthen `persistent_sep_dup` to support propositions that are persistent
and either affine or absorbing.
* Fix the statement of the lemma `fupd_plainly_laterN`; the old lemma was a
duplicate of `fupd_plain_laterN`.
**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