diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1c497ad9074d7af96463077776dc7eef00577ac..84c3259c05c85dc2efbd2ff3e69570e1a32421b6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -198,6 +198,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 * Add lemmas `inv_combine` and `inv_combine_dup_l` for combining invariants.
 * Rename `heap_lang.lifting` to `heap_lang.primitive_laws`. There now also
   exists `heap_lang.derived_laws`.
+* Remove global `Open Scope Z_scope` from `heap_lang.lang`, and leave it up to
+  reverse dependencies if they want to `Open Scope Z_scope` or not.
 
 The following `sed` script should perform most of the renaming (FIXME: incomplete)
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):