diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4282a3886127b7e3847a0a4aec7079a3a2030846..be6bccf5e6473faf281a8d08b5dae2a50e2633a2 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