From efbdb223b3329d6cae0cecebdb6d98453fb489d4 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 12 Sep 2018 14:49:06 +0200
Subject: Statement of `bool_irrelevance` more consistent with its name.

---
 ChangeLog | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'ChangeLog')

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
-- 
cgit v1.2.3