From fd83e4682f1a69a0e068df20128a979d75198d5c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 21 Aug 2016 14:51:32 +0200
Subject: [PATCH] document that units no logner have to be concrete

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 892ad8cc2..7dfe2cbeb 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,6 +9,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   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.
+* [#] With invariants and the physical state being handled in the logic, there
+  is no longer any reason to demand the CMRA unit to be discrete.
 * [#] The language can now fork off multiple threads at once.
 
 ## Iris 2.0
-- 
GitLab