From 9c8f15339e719321d1a04360d3d2052ecd8bb5a2 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 20 Mar 2019 18:31:45 +0100
Subject: Compat of sumn with bigop and renaming dep to cond when appropriate

---
 ChangeLog | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index 81d479a..0a5e310 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -95,6 +95,16 @@
 
 	* Corrected implicits and documentation of MatrixGenField.
 
+	* Renamed `big_setIDdep` to `big_setIDcond`
+	  and `sum_nat_dep_const` to `sum_nat_cond_const`
+
+	* Added lemmas `big_imset_cond`,`big_map_id`, `big_image_cond`
+	  `big_image`, `big_image_cond_id` and `big_image_id` for
+	  completeness purposes
+
+	* Added lemmas `foldrE`, `foldlE`, `foldl_idx` and `sumnE`
+	  to turn "seq statements" into "bigop statements"
+
 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