From 1262a001923f26f08f089dfaf8866c1ccd5d197c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 24 Nov 2017 15:41:18 +0100
Subject: [PATCH] update changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 37dad3892..ca6541a89 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -73,6 +73,10 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
     tactics now no longer work when the universal quantifier or modality is
     behind a type class opaque definition.  Furthermore, this can change the
     name of anonymous identifiers introduced with the "%" pattern.
+* Make `ofe_fun` dependently typed, subsuming `iprod`.  The latter got removed.
+* Generalize `saved_prop` to let the user choose the location of the type-level
+  later.  Rename the general form to `saved_anything`.  Provide `saved_prop` and
+  `saved_pred` as special cases.
 * 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.
-- 
GitLab