aboutsummaryrefslogtreecommitdiff
path: root/ChangeLog
diff options
context:
space:
mode:
Diffstat (limited to 'ChangeLog')
-rw-r--r--ChangeLog4
1 files changed, 4 insertions, 0 deletions
diff --git a/ChangeLog b/ChangeLog
index fc10b66..e37f1e8 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,4 +1,8 @@
??/??/???? - version 1.7.1
+
+ * Removed `_ : Type` field from packed classes. This performance
+ optimization is not strictly necessary with modern Coq versions.
+
* Added companion matrix of a polynomial `companionmx p` and the
theorems: companionmxK, map_mx_companion and companion_map_poly