diff --git a/CHANGELOG.md b/CHANGELOG.md index fdacba5fe4a793b0d7f43737ee3d92919e1eda00..bcbf9837333308d2cf4c3862da06fe91f7aab3d4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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`:**