diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2957ddba86ba933c428aee02543076de67a1264c..a11bd3dd394f5c93572485f8801d844ff3a2a881 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,7 +63,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Improvements to `BiMonoPred`:
   - Use `□`/`-∗` instead of `<pers>`/`→`.
   - Strengthen to ensure that functions for recursive calls are non-expansive.
-* Add `big_andM` with lemmas similar to `big_andL`.
+* Add `big_andM` (big conjunction on finite maps) with lemmas similar to `big_andL`.
 
 **Changes in `proofmode`:**