diff options
Diffstat (limited to 'ChangeLog')
| -rw-r--r-- | ChangeLog | 8 |
1 files changed, 8 insertions, 0 deletions
@@ -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 |