diff --git a/CHANGELOG.md b/CHANGELOG.md index 224d4dcbdb6892d2b0de6e2ab23a9e7220d49513..5ba909bf2fde70140e246dafdbfcd4f5e99d1853 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -55,6 +55,8 @@ lemma. `least_fixpoint_persistent_affine`, `least_fixpoint_persistent_absorbing`, `greatest_fixpoint_absorbing`. * Rename `laterN_plus` into `laterN_add`. +* Remove `make_laterable` from atomic updates. This relies on Iris now having + support for later credits (see below). **Changes in `proofmode`:**