update CHANGELOG

CHANGELOG.md

-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