From 6f647dd054e3f582f3b6375edb54677ff69164cc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 16 Sep 2020 12:06:01 +0200
Subject: [PATCH] add changelog entry

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 577fa1fa4..21f4246ed 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -40,6 +40,14 @@ With this release, we dropped support for Coq 8.9.
 
 * Add a `ghost_var` library that provides (fractional) ownership of a ghost
   variable of arbitrary `Type`.
+* Change type of some ghost state lemmas (mostly about allocation) to use `∗`
+  instead of `∧` (consistent with our usual style).  This affects the following
+  lemmas: `own_alloc_strong_dep`, `own_alloc_cofinite_dep`, `own_alloc_strong`,
+  `own_alloc_cofinite`, `own_updateP`, `saved_anything_alloc_strong`,
+  `saved_anything_alloc_cofinite`, `saved_prop_alloc_strong`,
+  `saved_prop_alloc_cofinite`, `saved_pred_alloc_strong`,
+  `saved_pred_alloc_cofinite`, `auth_alloc_strong`, `auth_alloc_cofinite`,
+  `auth_alloc`.
 
 The following `sed` script helps adjust your code to the renaming (on macOS,
 replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
-- 
GitLab