Merge pull request #235 from CohenCyril/bool_irrelevance2

Statement of `bool_irrelevance` more consistent with its name.

1 files changed, 3 insertions, 0 deletions

diff --git a/ChangeLog b/ChangeLog
index c651b13..00ab480 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -23,6 +23,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