From f6355c0594b878f651c83006a450e10c0f7c4104 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 9 Dec 2016 17:44:53 +0100
Subject: [PATCH] update changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fa2dfe454..b3463405b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,8 +10,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   backwards compatibility and will be removed in a future version of Iris.
 * View shifts are radically simplified to just internalize frame-preserving
   updates.  Weakestpre is defined inside the logic, and invariants and view
-  shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
-  is proven in the logic.
+  shifts with masks are also coded up inside Iris.  Adequacy of weakestpre is
+  proven in the logic. [#] The old ownership of the entire physical state is
+  replaced by a user-selected predicate over physical state that is maintained
+  by weakestpre.
 * Use OFEs instead of COFEs everywhere.  COFEs are only used for solving the
   recursive domain equation.  As a consequence, CMRAs no longer need a proof
   of completeness.
-- 
GitLab