From 825974bd94949449eed0e1efc224041499ab94e1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 Jul 2016 19:03:38 +0200
Subject: [PATCH] update CHANGELOG

---
 CHANGELOG.md | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4282a3886..be6bccf5e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,10 +1,17 @@
-In this changelog, we document "large-ish" changes to Iris that affect even the way the logic is used on paper.
-We do *not* document changesd of functions names or similar Coq-only API changes.
-Changes marked [*] still need to be ported to the Iris Documentation.
+In this changelog, we document "large-ish" changes to Iris that affect even the
+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.
 
 ## Iris 2.0
 
-[*] Make the core of an RA or CMRA a partial function.
+This version accompanies the final ICFP paper.
+
+* [# algebra] Make the core of an RA or CMRA a partial function.
+* [heap_lang] No longer use dependent types for expressions.  Instead, values
+  carry a proof of closedness.  Substitution, closedness and value-ness proofs
+  are performed by computation after reflecting into a term langauge that knows
+  about values and closed expressions.
 
 ## Iris 2.0-rc1
 
-- 
GitLab