aboutsummaryrefslogtreecommitdiff
path: root/ChangeLog
diff options
context:
space:
mode:
Diffstat (limited to 'ChangeLog')
-rw-r--r--ChangeLog5
1 files changed, 5 insertions, 0 deletions
diff --git a/ChangeLog b/ChangeLog
index d59a140..d6ea65f 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -2,6 +2,11 @@
* Added companion matrix of a polynomial `companionmx p` and the
theorems: companionmxK, map_mx_companion and companion_map_poly
+ * 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)
+ proved by circular implication P0 -> P1 -> ... -> Pn -> P0
+
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