From 2d032b5330adc7e7d7dcf0fb0daf593bffe280ec Mon Sep 17 00:00:00 2001
From: Assia Mahboubi
Date: Mon, 30 Nov 2015 15:52:24 +0100
Subject: Typos in comments.

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

(limited to 'mathcomp/ssreflect')

diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index ae634ba..ee721d3 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -246,7 +246,7 @@ Require Import ssrfun.
 (*        or predicate complement, as in predC.                               *)
 (*  CA -- left commutativity.                                                 *)
 (*   D -- predicate difference, as in predD.                                  *)
-(*   E -- elimination, as in negbEf : ~~ b = false -> b.                      *)
+(*   E -- elimination, as in negbFE : ~~ b = false -> b.                      *)
 (*   F or f -- boolean false, as in andbF : b && false = false.               *)
 (*   I -- left/right injectivity, as in addbI : right_injective addb,         *)
 (*        or predicate intersection, as in predI.                             *)
-- 
cgit v1.2.3