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 +++
 mathcomp/ssreflect/eqtype.v | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

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
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 7c2a48e..f32d390 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -274,7 +274,7 @@ Canonical bool_eqType := Eval hnf in EqType bool bool_eqMixin.
 
 Lemma eqbE : eqb = eq_op. Proof. by []. Qed.
 
-Lemma bool_irrelevance (x y : bool) (E E' : x = y) : E = E'.
+Lemma bool_irrelevance (b : bool) (p1 p2 : b) : p1 = p2.
 Proof. exact: eq_irrelevance. Qed.
 
 Lemma negb_add b1 b2 : ~~ (b1 (+) b2) = (b1 == b2).
-- 
cgit v1.2.3