From 9d99d63c26eed4df9b181442eb9c5725dd8a20ef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 28 May 2020 16:27:14 +0200
Subject: [PATCH] CHANGELOG entry.

---
 CHANGELOG.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1c497ad9..84c3259c0 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`):
-- 
GitLab