diff --git a/CHANGELOG.md b/CHANGELOG.md index f07e719dce927af0b0296b4010a70a165c05b854..44b2615815e09b6f48146807e01247c05f5d96dd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -56,6 +56,7 @@ Coq 8.11 is no longer supported in this version of Iris. - Use `fupd_intro _ _` for the new field `state_interp_mono` of `irisG`. - Some proofs using lifting lemmas and adequacy theorems need to be adapted to ignore the new step counter. +* Remove `wp_frame_wand_l`; add `wp_frame_wand` as more symmetric replacement. **Changes in `heap_lang`:**