CHANGELOG entry.

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`):