From 13f3876137b93ea1edc2e51d9f69f5c62f829e35 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 30 Oct 2016 15:06:07 +0100
Subject: [PATCH] CHANGELOG: mention the moving-things-around

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 40663365c..ba65c6596 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,14 +3,15 @@ way the logic is used on paper.  We also mention some significant changes in the
 Coq development, but not every API-breaking change is listed.  Changes marked
 `[#]` still need to be ported to the Iris Documentation LaTeX file(s).
 
-## Iris 3.0~rc1
-
-This version matches the ESOP submission.
+## Iris 3.0 (unfinished)
 
 * 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.
+* Renaming and moving things around: uPred and the rest of the base logic are
+  in [base_logic], while [program_logic] is for everything involving the
+  general Iris notion of a language.
 * 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.
-- 
GitLab