From 0f785cb80a555ce4109255819becb953a968cc8c Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Mon, 4 Mar 2019 16:53:55 +0100
Subject: ChangeLog update

Describe extension and warn about incompatibilities.
---
 ChangeLog | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index 14cb315..16d1102 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -113,6 +113,14 @@
 	  Generalized some lemmas in a backward compatible way.
 	  Some strictly more general lemmas now have suffix `_dep`.
 
+	* Generalised {ffun A -> R} to handle dependent functions, and to be
+	  structurally positive so it can be used in recursive inductive type
+	  definitions. Minor backward incompatibilities: fgraph f is no longer
+	  a field accessor, and no longer equal to val f as {ffun A -> R} is no
+	  longer a subType; some instances of finfun, ffunE, ffunK may not unify
+	  with a generic nondependent function type A -> ?R due to a bug in
+	  Coq < 8.10.
+
 24/04/2018 - compatibility with Coq 8.8 and several small fixes - version 1.7
 
 	* Added compatibility with Coq 8.8 and lost compatibility with
-- 
cgit v1.2.3