diff --git a/CHANGELOG.md b/CHANGELOG.md
index 768bf1001e50a7477a00ab99bf54d5930eb9619c..975a03aa634be405573e278f27908fb16723a5dc 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -36,6 +36,10 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Add support for destructing existentials with the intro pattern `[%x ...]`.
   (by Tej Chajed)
 
+**Changes in `bi`:**
+
+* Add lemmas characterizing big-ops over pure predicates (`big_sep*_pure*`).
+
 **Changes in `base_logic`:**
 
 * Add `ghost_map`, a logic-level library for a `gmap K V` with an authoritative