From 741c92b0a34815cc3eb9b219ab779ed798ca0069 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 5 Oct 2020 15:46:27 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 586806bef..0ac1d724a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -80,6 +80,13 @@ With this release, we dropped support for Coq 8.9.
   `saved_pred_alloc_cofinite`, `auth_alloc_strong`, `auth_alloc_cofinite`,
   `auth_alloc`.
 * Change `uPred_mono` to only require inclusion at the smaller step-index.
+* Put `iProp`/`iPreProp`-isomorphism into the `own` construction. This affects
+  clients that define higher-order ghost state constructions. Concretely, when
+  defining an `inG`, the functor no longer needs to be applied to `iPreProp`,
+  but should be applied to `iProp`. This avoids clients from having to push
+  through the `iProp`/`iPreProp`-isomorphism themselves, which is now handled
+  once and for all by the `own` construction.
+
 
 **Changes in `program_logic`:**
 
-- 
GitLab