Refactoring allpairs to handle the dependent version as well

1 files changed, 8 insertions, 0 deletions

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