aboutsummaryrefslogtreecommitdiff
path: root/ChangeLog
diff options
context:
space:
mode:
authorCyril Cohen2018-09-12 14:49:06 +0200
committerCyril Cohen2018-10-26 10:22:44 +0200
commitefbdb223b3329d6cae0cecebdb6d98453fb489d4 (patch)
treecf54971f580b3f77504e3c9623700c718e2bbe3c /ChangeLog
parent76fb3c00580488f75362153f6ea252f9b4d4084b (diff)
Statement of `bool_irrelevance` more consistent with its name.
Diffstat (limited to 'ChangeLog')
-rw-r--r--ChangeLog3
1 files changed, 3 insertions, 0 deletions
diff --git a/ChangeLog b/ChangeLog
index 2e8a495..892ee68 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -14,6 +14,9 @@
* Removed duplicated definitions of `tag` `tagged` and `Tagged`
from eqtype.v. They were already in ssrfun.v.
+ * Specialized `bool_irrelevance` so that the statement reflects
+ the name
+
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