Adding allsigs, the dependent version of allpairs

1 files changed, 4 insertions, 0 deletions

diff --git a/ChangeLog b/ChangeLog
index d6ea65f..a9650bc 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,7 +1,11 @@
 ??/??/???? - version 1.7.1
+
 	* Added companion matrix of a polynomial `companionmx p` and the
 	  theorems: companionmxK, map_mx_companion and companion_map_poly
 
+	* Added allsigs, the dependent version of allpairs,
+	  with notation `[seq E | i <- s & j <- t]`
+
 	* Added all_iff, "the following are all equivalent"
 	  with notation [<-> P0; P1; ..; Pn] and theorems
 	  `all_iffLR` and coercion `all_iffP` (see header for doc)