From bb20d7a823888babc7f7d0580e3ef3402118edb8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 23 Nov 2017 17:52:31 +0100
Subject: [PATCH] Add Changelog entry.

---
 CHANGELOG.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a3305d696..7ff953ed4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -76,6 +76,11 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Define the generic `fill` operation of the `ectxi_language` construct in terms
   of a left fold instead of a right fold. This gives rise to more definitional
   equalities.
+* The language hierarchy (`language`, `ectx_language`, `ectxi_language`) is now
+  fully formalized using canonical structures instead of using a mixture of
+  type classes and canonical structures. Also, it now uses explicit mixins. The
+  file `program_logic/ectxi_language` contains some documentation on how to
+  setup Iris for your language.
 * Improved big operators:
   + They are no longer tied to cameras, but work on any monoid
   + The version of big operations over lists was redefined so that it enjoys
-- 
GitLab