From 7453c9260c49710d1d2732a61fbca7feadf8502e Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 27 Jul 2016 17:55:33 +0200
Subject: [PATCH] add missing item to CHANGELOG

---
 CHANGELOG.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3853fde16..13fa9bd61 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,13 +7,19 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 This version accompanies the final ICFP paper.
 
-* [# algebra] Make the core of an RA or CMRA a partial function.
+* [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.
 * [program_logic/language] The language does not define its own "atomic"
   predicate.  Instead, atomicity is defined as reducing in one step to a value.
+* [# program_logic/lifting] Lifting lemmas no longer round-trip through a
+  user-chosen predicate to define the configurations we can reduce to; they
+  directly relate to the operational semantics.  This is equivalent and
+  much simpler to read.
+  Due to a lack of maintenance and usefulness, lifting lemmas for Hoare triples
+  are removed.
 
 ## Iris 2.0-rc1
 
-- 
GitLab