aboutsummaryrefslogtreecommitdiff
path: root/ChangeLog
diff options
context:
space:
mode:
authorAnton Trunov2018-12-06 17:58:41 +0100
committerAnton Trunov2018-12-06 17:58:41 +0100
commit7ae08ee81c6859fb7ee4043207d87572a4bc3bc3 (patch)
treea54cd823592f397d744fb7c17449c1d6a333ab74 /ChangeLog
parentefbcb84f3ddfea53b7b914284d8fa80fdb7a56fd (diff)
Update ChangeLog
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