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

---
 doc/changelog/10-standard-library/12484-fix12483.rst |  6 ++++++
 test-suite/bugs/closed/bug_12483.v                   | 10 ++++++++++
 theories/Floats/SpecFloat.v                          |  2 +-
 3 files changed, 17 insertions(+), 1 deletion(-)
 create mode 100644 doc/changelog/10-standard-library/12484-fix12483.rst
 create mode 100644 test-suite/bugs/closed/bug_12483.v

diff --git a/doc/changelog/10-standard-library/12484-fix12483.rst b/doc/changelog/10-standard-library/12484-fix12483.rst
new file mode 100644
index 0000000000..95e7c150a3
--- /dev/null
+++ b/doc/changelog/10-standard-library/12484-fix12483.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Fix the specification of :n:`PrimFloat.leb` which made
+  :n:`(x <= y)%float` true for any non NaN :n:`x` and :n:`y`.
+  (`#12484 <https://github.com/coq/coq/pull/12484>`_,
+  fixes `#12483 <https://github.com/coq/coq/issues/12483>`_,
+  by Pierre Roux).
diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v
new file mode 100644
index 0000000000..0d034a65eb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12483.v
@@ -0,0 +1,10 @@
+Require Import Floats.
+
+Goal False.
+Proof.
+cut (false = true).
+{ intro H; discriminate H. }
+change false with (1 <= 0)%float.
+rewrite leb_spec.
+Fail reflexivity.
+Abort.
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