From 8ecdb858a416b945fd9bc429e9eecf8aa451f0e7 Mon Sep 17 00:00:00 2001
From: Pierre Roux
Date: Mon, 8 Jun 2020 18:17:30 +0200
Subject: Fix 12483

---
 theories/Floats/SpecFloat.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Floats/SpecFloat.v b/theories/Floats/SpecFloat.v
index 349b37c704..aaf7cbb8f7 100644
--- a/theories/Floats/SpecFloat.v
+++ b/theories/Floats/SpecFloat.v
@@ -222,7 +222,7 @@ Section FloatOps.
 
   Definition SFleb f1 f2 :=
     match SFcompare f1 f2 with
-    | Some Le => true
+    | Some (Lt | Eq) => true
     | _ => false
     end.
 
-- 
cgit v1.2.3