diff --git a/CHANGELOG.md b/CHANGELOG.md
index d7c576cc6518d45494e6dd530d1b5f3c840f20f1..df598d46245d05a7a68b13e0221fe6f3d97c12b5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -59,6 +59,7 @@ Coq 8.11 is no longer supported in this version of Iris.
     As a consequence, `make_laterable_elim` got weaker: elimination now requires
     an except-0 modality (`make_laterable P -∗ ◇ P`).
   - Add `iModIntro` support for `make_laterable`.
+* State `bi_mono_pred` using `□`/`-∗` instead of `<pers>`/`→`.
 
 **Changes in `proofmode`:**