From d6dbcfe8edacdf00df988843ed6b74ecfc2db744 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 20 Mar 2019 18:22:20 +0100
Subject: Refactoring allpairs to handle the dependent version as well

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

(limited to 'ChangeLog')

diff --git a/ChangeLog b/ChangeLog
index 0a5e310..14cb315 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -105,6 +105,14 @@
 	* Added lemmas `foldrE`, `foldlE`, `foldl_idx` and `sumnE`
 	  to turn "seq statements" into "bigop statements"
 
+	* Generalized the notation `[seq E | i <- s, j <- t]` to the case
+	  where `t` may depend on `i`. The notation is now primitive and
+	  expressed using `flatten` and `map` (see documentation of seq).
+	  `allpairs` now expands to this notation when fully applied.
+	  Added `allpairs_dep` and made it self-expanding as well.
+	  Generalized some lemmas in a backward compatible way.
+	  Some strictly more general lemmas now have suffix `_dep`.
+
 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