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.

---
 mathcomp/ssreflect/eqtype.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp')

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