From fcc3db46303d97e0696a1685619301be3622f4e9 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sat, 20 Jun 2020 23:35:53 -0400
Subject: Bring Float notations in line with stdlib

This is a companion to #12479 as per
https://github.com/coq/coq/pull/12479#issuecomment-641336039 that
changes some of the PrimFloat notations:
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere

We also put them in a module, so users can `Require PrimFloat. Import
PrimFloat.PrimFloatNotations` without needing to unqualify the
primitives.

Fixes the part of #12454 about floats
---
 .../12556-fix-float-ltb-notations.rst              |   9 +
 doc/sphinx/language/coq-library.rst                |  42 +-
 test-suite/bugs/closed/bug_12483.v                 |   2 +-
 test-suite/primitive/float/compare.v               | 504 ++++++++++-----------
 test-suite/primitive/float/gen_compare.sh          |   2 +-
 theories/Floats/FloatAxioms.v                      |   6 +-
 theories/Floats/PrimFloat.v                        |  41 +-
 7 files changed, 316 insertions(+), 290 deletions(-)
 create mode 100644 doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst

diff --git a/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst
new file mode 100644
index 0000000000..1709cf1eae
--- /dev/null
+++ b/doc/changelog/10-standard-library/12556-fix-float-ltb-notations.rst
@@ -0,0 +1,9 @@
+- **Changed:**
+  PrimFloat notations now match up with the rest of the standard library: :g:`m
+  == n`, :g:`m < n`, and :g:`m <= n` have been replaced with :g:`m =? n`, :g:`m
+  <? n`, and :g:`m <=? n`.  The old notations are still available as deprecated
+  notations.  Additionally, there is now a
+  ``Coq.Floats.PrimFloat.PrimFloatNotations`` module that users can import to
+  get the ``PrimFloat`` notations without unqualifying the various primitives
+  (`#12556 <https://github.com/coq/coq/pull/12556>`_, fixes `#12454
+  <https://github.com/coq/coq/issues/12454>`_, by Jason Gross).
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index f9d24fde0e..c27eb216e8 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -40,7 +40,7 @@ in the |Coq| root directory; this includes the modules
 ``Datatypes``,
 ``Specif``,
 ``Peano``,
-``Wf`` and 
+``Wf`` and
 ``Tactics``.
 Module ``Logic_Type`` also makes it in the initial state.
 
@@ -175,7 +175,7 @@ Quantifiers
 Then we find first-order quantifiers:
 
 .. coqtop:: in
-  
+
    Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
    Inductive ex (A: Set) (P:A -> Prop) : Prop :=
     ex_intro (x:A) (_:P x).
@@ -256,12 +256,12 @@ Finally, a few easy lemmas are provided.
   single: f_equal2 ... f_equal5 (term)
 
 The theorem ``f_equal`` is extended to functions with two to five
-arguments. The theorem are names ``f_equal2``, ``f_equal3``, 
+arguments. The theorem are names ``f_equal2``, ``f_equal3``,
 ``f_equal4`` and ``f_equal5``.
 For instance ``f_equal3`` is defined the following way.
 
 .. coqtop:: in abort
-  
+
   Theorem f_equal3 :
    forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B)
      (x1 y1:A1) (x2 y2:A2) (x3 y3:A3),
@@ -324,7 +324,7 @@ Programming
 
 Note that zero is the letter ``O``, and *not* the numeral ``0``.
 
-The predicate ``identity`` is logically 
+The predicate ``identity`` is logically
 equivalent to equality but it lives in sort ``Type``.
 It is mainly maintained for compatibility.
 
@@ -367,7 +367,7 @@ infix notation ``||``), ``xorb``, ``implb`` and ``negb``.
 Specification
 ~~~~~~~~~~~~~
 
-The following notions defined in module ``Specif.v`` allow to build new data-types and specifications. 
+The following notions defined in module ``Specif.v`` allow to build new data-types and specifications.
 They are available with the syntax shown in the previous section :ref:`datatypes`.
 
 For instance, given :g:`A:Type` and :g:`P:A->Prop`, the construct
@@ -393,11 +393,11 @@ provided.
 .. coqtop:: in
 
   Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
-  Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
+  Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
     exist2 (x:A) (_:P x) (_:Q x).
 
 A *strong (dependent) sum* :g:`{x:A & P x}` may be also defined,
-when the predicate ``P`` is now defined as a 
+when the predicate ``P`` is now defined as a
 constructor of types in ``Type``.
 
 .. index::
@@ -556,7 +556,7 @@ section :tacn:`refine`). This scope is opened by default.
 Now comes the content of module ``Peano``:
 
 .. coqdoc::
-  
+
   Theorem eq_S : forall x y:nat, x = y -> S x = S y.
   Definition pred (n:nat) : nat :=
    match n with
@@ -628,7 +628,7 @@ induction principle.
 .. coqdoc::
 
   Theorem nat_case :
-   forall (n:nat) (P:nat -> Prop), 
+   forall (n:nat) (P:nat -> Prop),
    P 0 -> (forall m:nat, P (S m)) -> P n.
   Theorem nat_double_ind :
    forall R:nat -> nat -> Prop,
@@ -640,7 +640,7 @@ induction principle.
 Well-founded recursion
 ~~~~~~~~~~~~~~~~~~~~~~
 
-The basic library contains the basics of well-founded recursion and 
+The basic library contains the basics of well-founded recursion and
 well-founded induction, in module ``Wf.v``.
 
 .. index::
@@ -669,7 +669,7 @@ well-founded induction, in module ``Wf.v``.
    forall P:A -> Prop,
     (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 
-The automatically generated scheme ``Acc_rect`` 
+The automatically generated scheme ``Acc_rect``
 can be used to define functions by fixpoints using
 well-founded relations to justify termination. Assuming
 extensionality of the functional used for the recursive call, the
@@ -741,7 +741,7 @@ The standard library
 Survey
 ~~~~~~
 
-The rest of the standard library is structured into the following 
+The rest of the standard library is structured into the following
 subdirectories:
 
   * **Logic** : Classical logic and dependent equality
@@ -751,8 +751,8 @@ subdirectories:
   * **ZArith** : Basic relative integer arithmetic
   * **Numbers** : Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2^31 binary words)
   * **Bool** : Booleans (basic functions and results)
-  * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) 
-  * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.) 
+  * **Lists** : Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types)
+  * **Sets** : Sets (classical, constructive, finite, infinite, power set, etc.)
   * **FSets** : Specification and implementations of finite sets and finite maps (by lists and by AVL trees)
   * **Reals** : Axiomatization of real numbers (classical, basic functions, integer part, fractional part, limit, derivative, Cauchy series, power series and results,...)
   * **Floats** : Machine implementation of floating-point arithmetic (for the binary64 format)
@@ -903,7 +903,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
 
 .. tacn:: discrR
   :name: discrR
-  
+
   Proves that two real integer constants are different.
 
 .. example::
@@ -931,7 +931,7 @@ tactics (see Chapter :ref:`tactics`), there are also:
 
 .. tacn:: split_Rmult
   :name: split_Rmult
- 
+
   Splits a condition that a product is non null into subgoals
   corresponding to the condition on each operand of the product.
 
@@ -963,7 +963,7 @@ List library
   single: fold_left (term)
   single: fold_right (term)
 
-Some elementary operations on polymorphic lists are defined here. 
+Some elementary operations on polymorphic lists are defined here.
 They can be accessed by requiring module ``List``.
 
 It defines the following notions:
@@ -1052,9 +1052,9 @@ Notation     Interpretation
 ``_ + _``    ``add``
 ``_ * _``    ``mul``
 ``_ / _``    ``div``
-``_ == _``   ``eqb``
-``_ < _``    ``ltb``
-``_ <= _``   ``leb``
+``_ =? _``   ``eqb``
+``_ <? _``    ``ltb``
+``_ <=? _``   ``leb``
 ``_ ?= _``   ``compare``
 ===========  ==============
 
diff --git a/test-suite/bugs/closed/bug_12483.v b/test-suite/bugs/closed/bug_12483.v
index 0d034a65eb..ae46117e59 100644
--- a/test-suite/bugs/closed/bug_12483.v
+++ b/test-suite/bugs/closed/bug_12483.v
@@ -4,7 +4,7 @@ Goal False.
 Proof.
 cut (false = true).
 { intro H; discriminate H. }
-change false with (1 <= 0)%float.
+change false with (1 <=? 0)%float.
 rewrite leb_spec.
 Fail reflexivity.
 Abort.
diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v
index 23d1e5bbae..75fd5c426f 100644
--- a/test-suite/primitive/float/compare.v
+++ b/test-suite/primitive/float/compare.v
@@ -6,380 +6,380 @@ Definition min_denorm := Eval compute in ldexp one (-1074)%Z.
 
 Definition min_norm := Eval compute in ldexp one (-1024)%Z.
 
-Check (eq_refl false : nan == nan = false).
-Check (eq_refl false : nan == nan = false).
-Check (eq_refl false : nan < nan = false).
-Check (eq_refl false : nan < nan = false).
-Check (eq_refl false : nan <= nan = false).
-Check (eq_refl false : nan <= nan = false).
+Check (eq_refl false : nan =? nan = false).
+Check (eq_refl false : nan =? nan = false).
+Check (eq_refl false : nan <? nan = false).
+Check (eq_refl false : nan <? nan = false).
+Check (eq_refl false : nan <=? nan = false).
+Check (eq_refl false : nan <=? nan = false).
 Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).
 Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).
 
-Check (eq_refl false <: nan == nan = false).
-Check (eq_refl false <: nan == nan = false).
-Check (eq_refl false <: nan < nan = false).
-Check (eq_refl false <: nan < nan = false).
-Check (eq_refl false <: nan <= nan = false).
-Check (eq_refl false <: nan <= nan = false).
+Check (eq_refl false <: nan =? nan = false).
+Check (eq_refl false <: nan =? nan = false).
+Check (eq_refl false <: nan <? nan = false).
+Check (eq_refl false <: nan <? nan = false).
+Check (eq_refl false <: nan <=? nan = false).
+Check (eq_refl false <: nan <=? nan = false).
 Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).
 Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).
 
-Check (eq_refl false <<: nan == nan = false).
-Check (eq_refl false <<: nan == nan = false).
-Check (eq_refl false <<: nan < nan = false).
-Check (eq_refl false <<: nan < nan = false).
-Check (eq_refl false <<: nan <= nan = false).
-Check (eq_refl false <<: nan <= nan = false).
+Check (eq_refl false <<: nan =? nan = false).
+Check (eq_refl false <<: nan =? nan = false).
+Check (eq_refl false <<: nan <? nan = false).
+Check (eq_refl false <<: nan <? nan = false).
+Check (eq_refl false <<: nan <=? nan = false).
+Check (eq_refl false <<: nan <=? nan = false).
 Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).
 Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).
 
-Check (eq_refl false : nan == - nan = false).
-Check (eq_refl false : - nan == nan = false).
-Check (eq_refl false : nan < - nan = false).
-Check (eq_refl false : - nan < nan = false).
-Check (eq_refl false : nan <= - nan = false).
-Check (eq_refl false : - nan <= nan = false).
+Check (eq_refl false : nan =? - nan = false).
+Check (eq_refl false : - nan =? nan = false).
+Check (eq_refl false : nan <? - nan = false).
+Check (eq_refl false : - nan <? nan = false).
+Check (eq_refl false : nan <=? - nan = false).
+Check (eq_refl false : - nan <=? nan = false).
 Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable).
 Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable).
 
-Check (eq_refl false <: nan == - nan = false).
-Check (eq_refl false <: - nan == nan = false).
-Check (eq_refl false <: nan < - nan = false).
-Check (eq_refl false <: - nan < nan = false).
-Check (eq_refl false <: nan <= - nan = false).
-Check (eq_refl false <: - nan <= nan = false).
+Check (eq_refl false <: nan =? - nan = false).
+Check (eq_refl false <: - nan =? nan = false).
+Check (eq_refl false <: nan <? - nan = false).
+Check (eq_refl false <: - nan <? nan = false).
+Check (eq_refl false <: nan <=? - nan = false).
+Check (eq_refl false <: - nan <=? nan = false).
 Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable).
 Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable).
 
-Check (eq_refl false <<: nan == - nan = false).
-Check (eq_refl false <<: - nan == nan = false).
-Check (eq_refl false <<: nan < - nan = false).
-Check (eq_refl false <<: - nan < nan = false).
-Check (eq_refl false <<: nan <= - nan = false).
-Check (eq_refl false <<: - nan <= nan = false).
+Check (eq_refl false <<: nan =? - nan = false).
+Check (eq_refl false <<: - nan =? nan = false).
+Check (eq_refl false <<: nan <? - nan = false).
+Check (eq_refl false <<: - nan <? nan = false).
+Check (eq_refl false <<: nan <=? - nan = false).
+Check (eq_refl false <<: - nan <=? nan = false).
 Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable).
 Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable).
 
-Check (eq_refl true : one == one = true).
-Check (eq_refl true : one == one = true).
-Check (eq_refl false : one < one = false).
-Check (eq_refl false : one < one = false).
-Check (eq_refl true : one <= one = true).
-Check (eq_refl true : one <= one = true).
+Check (eq_refl true : one =? one = true).
+Check (eq_refl true : one =? one = true).
+Check (eq_refl false : one <? one = false).
+Check (eq_refl false : one <? one = false).
+Check (eq_refl true : one <=? one = true).
+Check (eq_refl true : one <=? one = true).
 Check (eq_refl FEq : one ?= one = FEq).
 Check (eq_refl FEq : one ?= one = FEq).
 
-Check (eq_refl true <: one == one = true).
-Check (eq_refl true <: one == one = true).
-Check (eq_refl false <: one < one = false).
-Check (eq_refl false <: one < one = false).
-Check (eq_refl true <: one <= one = true).
-Check (eq_refl true <: one <= one = true).
+Check (eq_refl true <: one =? one = true).
+Check (eq_refl true <: one =? one = true).
+Check (eq_refl false <: one <? one = false).
+Check (eq_refl false <: one <? one = false).
+Check (eq_refl true <: one <=? one = true).
+Check (eq_refl true <: one <=? one = true).
 Check (eq_refl FEq <: one ?= one = FEq).
 Check (eq_refl FEq <: one ?= one = FEq).
 
-Check (eq_refl true <<: one == one = true).
-Check (eq_refl true <<: one == one = true).
-Check (eq_refl false <<: one < one = false).
-Check (eq_refl false <<: one < one = false).
-Check (eq_refl true <<: one <= one = true).
-Check (eq_refl true <<: one <= one = true).
+Check (eq_refl true <<: one =? one = true).
+Check (eq_refl true <<: one =? one = true).
+Check (eq_refl false <<: one <? one = false).
+Check (eq_refl false <<: one <? one = false).
+Check (eq_refl true <<: one <=? one = true).
+Check (eq_refl true <<: one <=? one = true).
 Check (eq_refl FEq <<: one ?= one = FEq).
 Check (eq_refl FEq <<: one ?= one = FEq).
 
-Check (eq_refl true : zero == zero = true).
-Check (eq_refl true : zero == zero = true).
-Check (eq_refl false : zero < zero = false).
-Check (eq_refl false : zero < zero = false).
-Check (eq_refl true : zero <= zero = true).
-Check (eq_refl true : zero <= zero = true).
+Check (eq_refl true : zero =? zero = true).
+Check (eq_refl true : zero =? zero = true).
+Check (eq_refl false : zero <? zero = false).
+Check (eq_refl false : zero <? zero = false).
+Check (eq_refl true : zero <=? zero = true).
+Check (eq_refl true : zero <=? zero = true).
 Check (eq_refl FEq : zero ?= zero = FEq).
 Check (eq_refl FEq : zero ?= zero = FEq).
 
-Check (eq_refl true <: zero == zero = true).
-Check (eq_refl true <: zero == zero = true).
-Check (eq_refl false <: zero < zero = false).
-Check (eq_refl false <: zero < zero = false).
-Check (eq_refl true <: zero <= zero = true).
-Check (eq_refl true <: zero <= zero = true).
+Check (eq_refl true <: zero =? zero = true).
+Check (eq_refl true <: zero =? zero = true).
+Check (eq_refl false <: zero <? zero = false).
+Check (eq_refl false <: zero <? zero = false).
+Check (eq_refl true <: zero <=? zero = true).
+Check (eq_refl true <: zero <=? zero = true).
 Check (eq_refl FEq <: zero ?= zero = FEq).
 Check (eq_refl FEq <: zero ?= zero = FEq).
 
-Check (eq_refl true <<: zero == zero = true).
-Check (eq_refl true <<: zero == zero = true).
-Check (eq_refl false <<: zero < zero = false).
-Check (eq_refl false <<: zero < zero = false).
-Check (eq_refl true <<: zero <= zero = true).
-Check (eq_refl true <<: zero <= zero = true).
+Check (eq_refl true <<: zero =? zero = true).
+Check (eq_refl true <<: zero =? zero = true).
+Check (eq_refl false <<: zero <? zero = false).
+Check (eq_refl false <<: zero <? zero = false).
+Check (eq_refl true <<: zero <=? zero = true).
+Check (eq_refl true <<: zero <=? zero = true).
 Check (eq_refl FEq <<: zero ?= zero = FEq).
 Check (eq_refl FEq <<: zero ?= zero = FEq).
 
-Check (eq_refl true : zero == - zero = true).
-Check (eq_refl true : - zero == zero = true).
-Check (eq_refl false : zero < - zero = false).
-Check (eq_refl false : - zero < zero = false).
-Check (eq_refl true : zero <= - zero = true).
-Check (eq_refl true : - zero <= zero = true).
+Check (eq_refl true : zero =? - zero = true).
+Check (eq_refl true : - zero =? zero = true).
+Check (eq_refl false : zero <? - zero = false).
+Check (eq_refl false : - zero <? zero = false).
+Check (eq_refl true : zero <=? - zero = true).
+Check (eq_refl true : - zero <=? zero = true).
 Check (eq_refl FEq : zero ?= - zero = FEq).
 Check (eq_refl FEq : - zero ?= zero = FEq).
 
-Check (eq_refl true <: zero == - zero = true).
-Check (eq_refl true <: - zero == zero = true).
-Check (eq_refl false <: zero < - zero = false).
-Check (eq_refl false <: - zero < zero = false).
-Check (eq_refl true <: zero <= - zero = true).
-Check (eq_refl true <: - zero <= zero = true).
+Check (eq_refl true <: zero =? - zero = true).
+Check (eq_refl true <: - zero =? zero = true).
+Check (eq_refl false <: zero <? - zero = false).
+Check (eq_refl false <: - zero <? zero = false).
+Check (eq_refl true <: zero <=? - zero = true).
+Check (eq_refl true <: - zero <=? zero = true).
 Check (eq_refl FEq <: zero ?= - zero = FEq).
 Check (eq_refl FEq <: - zero ?= zero = FEq).
 
-Check (eq_refl true <<: zero == - zero = true).
-Check (eq_refl true <<: - zero == zero = true).
-Check (eq_refl false <<: zero < - zero = false).
-Check (eq_refl false <<: - zero < zero = false).
-Check (eq_refl true <<: zero <= - zero = true).
-Check (eq_refl true <<: - zero <= zero = true).
+Check (eq_refl true <<: zero =? - zero = true).
+Check (eq_refl true <<: - zero =? zero = true).
+Check (eq_refl false <<: zero <? - zero = false).
+Check (eq_refl false <<: - zero <? zero = false).
+Check (eq_refl true <<: zero <=? - zero = true).
+Check (eq_refl true <<: - zero <=? zero = true).
 Check (eq_refl FEq <<: zero ?= - zero = FEq).
 Check (eq_refl FEq <<: - zero ?= zero = FEq).
 
-Check (eq_refl true : - zero == - zero = true).
-Check (eq_refl true : - zero == - zero = true).
-Check (eq_refl false : - zero < - zero = false).
-Check (eq_refl false : - zero < - zero = false).
-Check (eq_refl true : - zero <= - zero = true).
-Check (eq_refl true : - zero <= - zero = true).
+Check (eq_refl true : - zero =? - zero = true).
+Check (eq_refl true : - zero =? - zero = true).
+Check (eq_refl false : - zero <? - zero = false).
+Check (eq_refl false : - zero <? - zero = false).
+Check (eq_refl true : - zero <=? - zero = true).
+Check (eq_refl true : - zero <=? - zero = true).
 Check (eq_refl FEq : - zero ?= - zero = FEq).
 Check (eq_refl FEq : - zero ?= - zero = FEq).
 
-Check (eq_refl true <: - zero == - zero = true).
-Check (eq_refl true <: - zero == - zero = true).
-Check (eq_refl false <: - zero < - zero = false).
-Check (eq_refl false <: - zero < - zero = false).
-Check (eq_refl true <: - zero <= - zero = true).
-Check (eq_refl true <: - zero <= - zero = true).
+Check (eq_refl true <: - zero =? - zero = true).
+Check (eq_refl true <: - zero =? - zero = true).
+Check (eq_refl false <: - zero <? - zero = false).
+Check (eq_refl false <: - zero <? - zero = false).
+Check (eq_refl true <: - zero <=? - zero = true).
+Check (eq_refl true <: - zero <=? - zero = true).
 Check (eq_refl FEq <: - zero ?= - zero = FEq).
 Check (eq_refl FEq <: - zero ?= - zero = FEq).
 
-Check (eq_refl true <<: - zero == - zero = true).
-Check (eq_refl true <<: - zero == - zero = true).
-Check (eq_refl false <<: - zero < - zero = false).
-Check (eq_refl false <<: - zero < - zero = false).
-Check (eq_refl true <<: - zero <= - zero = true).
-Check (eq_refl true <<: - zero <= - zero = true).
+Check (eq_refl true <<: - zero =? - zero = true).
+Check (eq_refl true <<: - zero =? - zero = true).
+Check (eq_refl false <<: - zero <? - zero = false).
+Check (eq_refl false <<: - zero <? - zero = false).
+Check (eq_refl true <<: - zero <=? - zero = true).
+Check (eq_refl true <<: - zero <=? - zero = true).
 Check (eq_refl FEq <<: - zero ?= - zero = FEq).
 Check (eq_refl FEq <<: - zero ?= - zero = FEq).
 
-Check (eq_refl true : infinity == infinity = true).
-Check (eq_refl true : infinity == infinity = true).
-Check (eq_refl false : infinity < infinity = false).
-Check (eq_refl false : infinity < infinity = false).
-Check (eq_refl true : infinity <= infinity = true).
-Check (eq_refl true : infinity <= infinity = true).
+Check (eq_refl true : infinity =? infinity = true).
+Check (eq_refl true : infinity =? infinity = true).
+Check (eq_refl false : infinity <? infinity = false).
+Check (eq_refl false : infinity <? infinity = false).
+Check (eq_refl true : infinity <=? infinity = true).
+Check (eq_refl true : infinity <=? infinity = true).
 Check (eq_refl FEq : infinity ?= infinity = FEq).
 Check (eq_refl FEq : infinity ?= infinity = FEq).
 
-Check (eq_refl true <: infinity == infinity = true).
-Check (eq_refl true <: infinity == infinity = true).
-Check (eq_refl false <: infinity < infinity = false).
-Check (eq_refl false <: infinity < infinity = false).
-Check (eq_refl true <: infinity <= infinity = true).
-Check (eq_refl true <: infinity <= infinity = true).
+Check (eq_refl true <: infinity =? infinity = true).
+Check (eq_refl true <: infinity =? infinity = true).
+Check (eq_refl false <: infinity <? infinity = false).
+Check (eq_refl false <: infinity <? infinity = false).
+Check (eq_refl true <: infinity <=? infinity = true).
+Check (eq_refl true <: infinity <=? infinity = true).
 Check (eq_refl FEq <: infinity ?= infinity = FEq).
 Check (eq_refl FEq <: infinity ?= infinity = FEq).
 
-Check (eq_refl true <<: infinity == infinity = true).
-Check (eq_refl true <<: infinity == infinity = true).
-Check (eq_refl false <<: infinity < infinity = false).
-Check (eq_refl false <<: infinity < infinity = false).
-Check (eq_refl true <<: infinity <= infinity = true).
-Check (eq_refl true <<: infinity <= infinity = true).
+Check (eq_refl true <<: infinity =? infinity = true).
+Check (eq_refl true <<: infinity =? infinity = true).
+Check (eq_refl false <<: infinity <? infinity = false).
+Check (eq_refl false <<: infinity <? infinity = false).
+Check (eq_refl true <<: infinity <=? infinity = true).
+Check (eq_refl true <<: infinity <=? infinity = true).
 Check (eq_refl FEq <<: infinity ?= infinity = FEq).
 Check (eq_refl FEq <<: infinity ?= infinity = FEq).
 
-Check (eq_refl true : - infinity == - infinity = true).
-Check (eq_refl true : - infinity == - infinity = true).
-Check (eq_refl false : - infinity < - infinity = false).
-Check (eq_refl false : - infinity < - infinity = false).
-Check (eq_refl true : - infinity <= - infinity = true).
-Check (eq_refl true : - infinity <= - infinity = true).
+Check (eq_refl true : - infinity =? - infinity = true).
+Check (eq_refl true : - infinity =? - infinity = true).
+Check (eq_refl false : - infinity <? - infinity = false).
+Check (eq_refl false : - infinity <? - infinity = false).
+Check (eq_refl true : - infinity <=? - infinity = true).
+Check (eq_refl true : - infinity <=? - infinity = true).
 Check (eq_refl FEq : - infinity ?= - infinity = FEq).
 Check (eq_refl FEq : - infinity ?= - infinity = FEq).
 
-Check (eq_refl true <: - infinity == - infinity = true).
-Check (eq_refl true <: - infinity == - infinity = true).
-Check (eq_refl false <: - infinity < - infinity = false).
-Check (eq_refl false <: - infinity < - infinity = false).
-Check (eq_refl true <: - infinity <= - infinity = true).
-Check (eq_refl true <: - infinity <= - infinity = true).
+Check (eq_refl true <: - infinity =? - infinity = true).
+Check (eq_refl true <: - infinity =? - infinity = true).
+Check (eq_refl false <: - infinity <? - infinity = false).
+Check (eq_refl false <: - infinity <? - infinity = false).
+Check (eq_refl true <: - infinity <=? - infinity = true).
+Check (eq_refl true <: - infinity <=? - infinity = true).
 Check (eq_refl FEq <: - infinity ?= - infinity = FEq).
 Check (eq_refl FEq <: - infinity ?= - infinity = FEq).
 
-Check (eq_refl true <<: - infinity == - infinity = true).
-Check (eq_refl true <<: - infinity == - infinity = true).
-Check (eq_refl false <<: - infinity < - infinity = false).
-Check (eq_refl false <<: - infinity < - infinity = false).
-Check (eq_refl true <<: - infinity <= - infinity = true).
-Check (eq_refl true <<: - infinity <= - infinity = true).
+Check (eq_refl true <<: - infinity =? - infinity = true).
+Check (eq_refl true <<: - infinity =? - infinity = true).
+Check (eq_refl false <<: - infinity <? - infinity = false).
+Check (eq_refl false <<: - infinity <? - infinity = false).
+Check (eq_refl true <<: - infinity <=? - infinity = true).
+Check (eq_refl true <<: - infinity <=? - infinity = true).
 Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).
 Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).
 
-Check (eq_refl false : min_denorm == min_norm = false).
-Check (eq_refl false : min_norm == min_denorm = false).
-Check (eq_refl true : min_denorm < min_norm = true).
-Check (eq_refl false : min_norm < min_denorm = false).
-Check (eq_refl true : min_denorm <= min_norm = true).
-Check (eq_refl false : min_norm <= min_denorm = false).
+Check (eq_refl false : min_denorm =? min_norm = false).
+Check (eq_refl false : min_norm =? min_denorm = false).
+Check (eq_refl true : min_denorm <? min_norm = true).
+Check (eq_refl false : min_norm <? min_denorm = false).
+Check (eq_refl true : min_denorm <=? min_norm = true).
+Check (eq_refl false : min_norm <=? min_denorm = false).
 Check (eq_refl FLt : min_denorm ?= min_norm = FLt).
 Check (eq_refl FGt : min_norm ?= min_denorm = FGt).
 
-Check (eq_refl false <: min_denorm == min_norm = false).
-Check (eq_refl false <: min_norm == min_denorm = false).
-Check (eq_refl true <: min_denorm < min_norm = true).
-Check (eq_refl false <: min_norm < min_denorm = false).
-Check (eq_refl true <: min_denorm <= min_norm = true).
-Check (eq_refl false <: min_norm <= min_denorm = false).
+Check (eq_refl false <: min_denorm =? min_norm = false).
+Check (eq_refl false <: min_norm =? min_denorm = false).
+Check (eq_refl true <: min_denorm <? min_norm = true).
+Check (eq_refl false <: min_norm <? min_denorm = false).
+Check (eq_refl true <: min_denorm <=? min_norm = true).
+Check (eq_refl false <: min_norm <=? min_denorm = false).
 Check (eq_refl FLt <: min_denorm ?= min_norm = FLt).
 Check (eq_refl FGt <: min_norm ?= min_denorm = FGt).
 
-Check (eq_refl false <<: min_denorm == min_norm = false).
-Check (eq_refl false <<: min_norm == min_denorm = false).
-Check (eq_refl true <<: min_denorm < min_norm = true).
-Check (eq_refl false <<: min_norm < min_denorm = false).
-Check (eq_refl true <<: min_denorm <= min_norm = true).
-Check (eq_refl false <<: min_norm <= min_denorm = false).
+Check (eq_refl false <<: min_denorm =? min_norm = false).
+Check (eq_refl false <<: min_norm =? min_denorm = false).
+Check (eq_refl true <<: min_denorm <? min_norm = true).
+Check (eq_refl false <<: min_norm <? min_denorm = false).
+Check (eq_refl true <<: min_denorm <=? min_norm = true).
+Check (eq_refl false <<: min_norm <=? min_denorm = false).
 Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt).
 Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt).
 
-Check (eq_refl false : min_denorm == one = false).
-Check (eq_refl false : one == min_denorm = false).
-Check (eq_refl true : min_denorm < one = true).
-Check (eq_refl false : one < min_denorm = false).
-Check (eq_refl true : min_denorm <= one = true).
-Check (eq_refl false : one <= min_denorm = false).
+Check (eq_refl false : min_denorm =? one = false).
+Check (eq_refl false : one =? min_denorm = false).
+Check (eq_refl true : min_denorm <? one = true).
+Check (eq_refl false : one <? min_denorm = false).
+Check (eq_refl true : min_denorm <=? one = true).
+Check (eq_refl false : one <=? min_denorm = false).
 Check (eq_refl FLt : min_denorm ?= one = FLt).
 Check (eq_refl FGt : one ?= min_denorm = FGt).
 
-Check (eq_refl false <: min_denorm == one = false).
-Check (eq_refl false <: one == min_denorm = false).
-Check (eq_refl true <: min_denorm < one = true).
-Check (eq_refl false <: one < min_denorm = false).
-Check (eq_refl true <: min_denorm <= one = true).
-Check (eq_refl false <: one <= min_denorm = false).
+Check (eq_refl false <: min_denorm =? one = false).
+Check (eq_refl false <: one =? min_denorm = false).
+Check (eq_refl true <: min_denorm <? one = true).
+Check (eq_refl false <: one <? min_denorm = false).
+Check (eq_refl true <: min_denorm <=? one = true).
+Check (eq_refl false <: one <=? min_denorm = false).
 Check (eq_refl FLt <: min_denorm ?= one = FLt).
 Check (eq_refl FGt <: one ?= min_denorm = FGt).
 
-Check (eq_refl false <<: min_denorm == one = false).
-Check (eq_refl false <<: one == min_denorm = false).
-Check (eq_refl true <<: min_denorm < one = true).
-Check (eq_refl false <<: one < min_denorm = false).
-Check (eq_refl true <<: min_denorm <= one = true).
-Check (eq_refl false <<: one <= min_denorm = false).
+Check (eq_refl false <<: min_denorm =? one = false).
+Check (eq_refl false <<: one =? min_denorm = false).
+Check (eq_refl true <<: min_denorm <? one = true).
+Check (eq_refl false <<: one <? min_denorm = false).
+Check (eq_refl true <<: min_denorm <=? one = true).
+Check (eq_refl false <<: one <=? min_denorm = false).
 Check (eq_refl FLt <<: min_denorm ?= one = FLt).
 Check (eq_refl FGt <<: one ?= min_denorm = FGt).
 
-Check (eq_refl false : min_norm == one = false).
-Check (eq_refl false : one == min_norm = false).
-Check (eq_refl true : min_norm < one = true).
-Check (eq_refl false : one < min_norm = false).
-Check (eq_refl true : min_norm <= one = true).
-Check (eq_refl false : one <= min_norm = false).
+Check (eq_refl false : min_norm =? one = false).
+Check (eq_refl false : one =? min_norm = false).
+Check (eq_refl true : min_norm <? one = true).
+Check (eq_refl false : one <? min_norm = false).
+Check (eq_refl true : min_norm <=? one = true).
+Check (eq_refl false : one <=? min_norm = false).
 Check (eq_refl FLt : min_norm ?= one = FLt).
 Check (eq_refl FGt : one ?= min_norm = FGt).
 
-Check (eq_refl false <: min_norm == one = false).
-Check (eq_refl false <: one == min_norm = false).
-Check (eq_refl true <: min_norm < one = true).
-Check (eq_refl false <: one < min_norm = false).
-Check (eq_refl true <: min_norm <= one = true).
-Check (eq_refl false <: one <= min_norm = false).
+Check (eq_refl false <: min_norm =? one = false).
+Check (eq_refl false <: one =? min_norm = false).
+Check (eq_refl true <: min_norm <? one = true).
+Check (eq_refl false <: one <? min_norm = false).
+Check (eq_refl true <: min_norm <=? one = true).
+Check (eq_refl false <: one <=? min_norm = false).
 Check (eq_refl FLt <: min_norm ?= one = FLt).
 Check (eq_refl FGt <: one ?= min_norm = FGt).
 
-Check (eq_refl false <<: min_norm == one = false).
-Check (eq_refl false <<: one == min_norm = false).
-Check (eq_refl true <<: min_norm < one = true).
-Check (eq_refl false <<: one < min_norm = false).
-Check (eq_refl true <<: min_norm <= one = true).
-Check (eq_refl false <<: one <= min_norm = false).
+Check (eq_refl false <<: min_norm =? one = false).
+Check (eq_refl false <<: one =? min_norm = false).
+Check (eq_refl true <<: min_norm <? one = true).
+Check (eq_refl false <<: one <? min_norm = false).
+Check (eq_refl true <<: min_norm <=? one = true).
+Check (eq_refl false <<: one <=? min_norm = false).
 Check (eq_refl FLt <<: min_norm ?= one = FLt).
 Check (eq_refl FGt <<: one ?= min_norm = FGt).
 
-Check (eq_refl false : one == infinity = false).
-Check (eq_refl false : infinity == one = false).
-Check (eq_refl true : one < infinity = true).
-Check (eq_refl false : infinity < one = false).
-Check (eq_refl true : one <= infinity = true).
-Check (eq_refl false : infinity <= one = false).
+Check (eq_refl false : one =? infinity = false).
+Check (eq_refl false : infinity =? one = false).
+Check (eq_refl true : one <? infinity = true).
+Check (eq_refl false : infinity <? one = false).
+Check (eq_refl true : one <=? infinity = true).
+Check (eq_refl false : infinity <=? one = false).
 Check (eq_refl FLt : one ?= infinity = FLt).
 Check (eq_refl FGt : infinity ?= one = FGt).
 
-Check (eq_refl false <: one == infinity = false).
-Check (eq_refl false <: infinity == one = false).
-Check (eq_refl true <: one < infinity = true).
-Check (eq_refl false <: infinity < one = false).
-Check (eq_refl true <: one <= infinity = true).
-Check (eq_refl false <: infinity <= one = false).
+Check (eq_refl false <: one =? infinity = false).
+Check (eq_refl false <: infinity =? one = false).
+Check (eq_refl true <: one <? infinity = true).
+Check (eq_refl false <: infinity <? one = false).
+Check (eq_refl true <: one <=? infinity = true).
+Check (eq_refl false <: infinity <=? one = false).
 Check (eq_refl FLt <: one ?= infinity = FLt).
 Check (eq_refl FGt <: infinity ?= one = FGt).
 
-Check (eq_refl false <<: one == infinity = false).
-Check (eq_refl false <<: infinity == one = false).
-Check (eq_refl true <<: one < infinity = true).
-Check (eq_refl false <<: infinity < one = false).
-Check (eq_refl true <<: one <= infinity = true).
-Check (eq_refl false <<: infinity <= one = false).
+Check (eq_refl false <<: one =? infinity = false).
+Check (eq_refl false <<: infinity =? one = false).
+Check (eq_refl true <<: one <? infinity = true).
+Check (eq_refl false <<: infinity <? one = false).
+Check (eq_refl true <<: one <=? infinity = true).
+Check (eq_refl false <<: infinity <=? one = false).
 Check (eq_refl FLt <<: one ?= infinity = FLt).
 Check (eq_refl FGt <<: infinity ?= one = FGt).
 
-Check (eq_refl false : - infinity == infinity = false).
-Check (eq_refl false : infinity == - infinity = false).
-Check (eq_refl true : - infinity < infinity = true).
-Check (eq_refl false : infinity < - infinity = false).
-Check (eq_refl true : - infinity <= infinity = true).
-Check (eq_refl false : infinity <= - infinity = false).
+Check (eq_refl false : - infinity =? infinity = false).
+Check (eq_refl false : infinity =? - infinity = false).
+Check (eq_refl true : - infinity <? infinity = true).
+Check (eq_refl false : infinity <? - infinity = false).
+Check (eq_refl true : - infinity <=? infinity = true).
+Check (eq_refl false : infinity <=? - infinity = false).
 Check (eq_refl FLt : - infinity ?= infinity = FLt).
 Check (eq_refl FGt : infinity ?= - infinity = FGt).
 
-Check (eq_refl false <: - infinity == infinity = false).
-Check (eq_refl false <: infinity == - infinity = false).
-Check (eq_refl true <: - infinity < infinity = true).
-Check (eq_refl false <: infinity < - infinity = false).
-Check (eq_refl true <: - infinity <= infinity = true).
-Check (eq_refl false <: infinity <= - infinity = false).
+Check (eq_refl false <: - infinity =? infinity = false).
+Check (eq_refl false <: infinity =? - infinity = false).
+Check (eq_refl true <: - infinity <? infinity = true).
+Check (eq_refl false <: infinity <? - infinity = false).
+Check (eq_refl true <: - infinity <=? infinity = true).
+Check (eq_refl false <: infinity <=? - infinity = false).
 Check (eq_refl FLt <: - infinity ?= infinity = FLt).
 Check (eq_refl FGt <: infinity ?= - infinity = FGt).
 
-Check (eq_refl false <<: - infinity == infinity = false).
-Check (eq_refl false <<: infinity == - infinity = false).
-Check (eq_refl true <<: - infinity < infinity = true).
-Check (eq_refl false <<: infinity < - infinity = false).
-Check (eq_refl true <<: - infinity <= infinity = true).
-Check (eq_refl false <<: infinity <= - infinity = false).
+Check (eq_refl false <<: - infinity =? infinity = false).
+Check (eq_refl false <<: infinity =? - infinity = false).
+Check (eq_refl true <<: - infinity <? infinity = true).
+Check (eq_refl false <<: infinity <? - infinity = false).
+Check (eq_refl true <<: - infinity <=? infinity = true).
+Check (eq_refl false <<: infinity <=? - infinity = false).
 Check (eq_refl FLt <<: - infinity ?= infinity = FLt).
 Check (eq_refl FGt <<: infinity ?= - infinity = FGt).
 
-Check (eq_refl false : - infinity == one = false).
-Check (eq_refl false : one == - infinity = false).
-Check (eq_refl true : - infinity < one = true).
-Check (eq_refl false : one < - infinity = false).
-Check (eq_refl true : - infinity <= one = true).
-Check (eq_refl false : one <= - infinity = false).
+Check (eq_refl false : - infinity =? one = false).
+Check (eq_refl false : one =? - infinity = false).
+Check (eq_refl true : - infinity <? one = true).
+Check (eq_refl false : one <? - infinity = false).
+Check (eq_refl true : - infinity <=? one = true).
+Check (eq_refl false : one <=? - infinity = false).
 Check (eq_refl FLt : - infinity ?= one = FLt).
 Check (eq_refl FGt : one ?= - infinity = FGt).
 
-Check (eq_refl false <: - infinity == one = false).
-Check (eq_refl false <: one == - infinity = false).
-Check (eq_refl true <: - infinity < one = true).
-Check (eq_refl false <: one < - infinity = false).
-Check (eq_refl true <: - infinity <= one = true).
-Check (eq_refl false <: one <= - infinity = false).
+Check (eq_refl false <: - infinity =? one = false).
+Check (eq_refl false <: one =? - infinity = false).
+Check (eq_refl true <: - infinity <? one = true).
+Check (eq_refl false <: one <? - infinity = false).
+Check (eq_refl true <: - infinity <=? one = true).
+Check (eq_refl false <: one <=? - infinity = false).
 Check (eq_refl FLt <: - infinity ?= one = FLt).
 Check (eq_refl FGt <: one ?= - infinity = FGt).
 
-Check (eq_refl false <<: - infinity == one = false).
-Check (eq_refl false <<: one == - infinity = false).
-Check (eq_refl true <<: - infinity < one = true).
-Check (eq_refl false <<: one < - infinity = false).
-Check (eq_refl true <<: - infinity <= one = true).
-Check (eq_refl false <<: one <= - infinity = false).
+Check (eq_refl false <<: - infinity =? one = false).
+Check (eq_refl false <<: one =? - infinity = false).
+Check (eq_refl true <<: - infinity <? one = true).
+Check (eq_refl false <<: one <? - infinity = false).
+Check (eq_refl true <<: - infinity <=? one = true).
+Check (eq_refl false <<: one <=? - infinity = false).
 Check (eq_refl FLt <<: - infinity ?= one = FLt).
 Check (eq_refl FGt <<: one ?= - infinity = FGt).
diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh
index cd87eb4e5b..6e3dd6d04b 100755
--- a/test-suite/primitive/float/gen_compare.sh
+++ b/test-suite/primitive/float/gen_compare.sh
@@ -20,7 +20,7 @@ genTest() {
         echo >&2 "genTest expects 10 arguments"
     fi
     TACTICS=(":" "<:" "<<:")
-    OPS=("==" "<" "<=" "?=")
+    OPS=("=?" "<?" "<=?" "?=")
     x="$1"
     y="$2"
     OPS1=("$3" "$4" "$5" "$6")  # for x y
diff --git a/theories/Floats/FloatAxioms.v b/theories/Floats/FloatAxioms.v
index f4aa1f81c6..78df357c0f 100644
--- a/theories/Floats/FloatAxioms.v
+++ b/theories/Floats/FloatAxioms.v
@@ -38,9 +38,9 @@ Qed.
 Axiom opp_spec : forall x, Prim2SF (-x)%float = SFopp (Prim2SF x).
 Axiom abs_spec : forall x, Prim2SF (abs x) = SFabs (Prim2SF x).
 
-Axiom eqb_spec : forall x y, (x == y)%float = SFeqb (Prim2SF x) (Prim2SF y).
-Axiom ltb_spec : forall x y, (x < y)%float = SFltb (Prim2SF x) (Prim2SF y).
-Axiom leb_spec : forall x y, (x <= y)%float = SFleb (Prim2SF x) (Prim2SF y).
+Axiom eqb_spec : forall x y, (x =? y)%float = SFeqb (Prim2SF x) (Prim2SF y).
+Axiom ltb_spec : forall x y, (x <? y)%float = SFltb (Prim2SF x) (Prim2SF y).
+Axiom leb_spec : forall x y, (x <=? y)%float = SFleb (Prim2SF x) (Prim2SF y).
 
 Definition flatten_cmp_opt c :=
   match c with
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v
index e5a9748481..ed7947aa63 100644
--- a/theories/Floats/PrimFloat.v
+++ b/theories/Floats/PrimFloat.v
@@ -27,9 +27,11 @@ Register float_class as kernel.ind_f_class.
 Primitive float := #float64_type.
 
 (** ** Syntax support *)
+Module Import PrimFloatNotationsInternalA.
 Declare Scope float_scope.
 Delimit Scope float_scope with float.
 Bind Scope float_scope with float.
+End PrimFloatNotationsInternalA.
 
 Declare ML Module "float_syntax_plugin".
 
@@ -41,31 +43,34 @@ Primitive abs := #float64_abs.
 Primitive sqrt := #float64_sqrt.
 
 Primitive opp := #float64_opp.
-Notation "- x" := (opp x) : float_scope.
 
 Primitive eqb := #float64_eq.
-Notation "x == y" := (eqb x y) (at level 70, no associativity) : float_scope.
 
 Primitive ltb := #float64_lt.
-Notation "x < y" := (ltb x y) (at level 70, no associativity) : float_scope.
 
 Primitive leb := #float64_le.
-Notation "x <= y" := (leb x y) (at level 70, no associativity) : float_scope.
 
 Primitive compare := #float64_compare.
-Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.
 
 Primitive mul := #float64_mul.
-Notation "x * y" := (mul x y) : float_scope.
 
 Primitive add := #float64_add.
-Notation "x + y" := (add x y) : float_scope.
 
 Primitive sub := #float64_sub.
-Notation "x - y" := (sub x y) : float_scope.
 
 Primitive div := #float64_div.
+
+Module Import PrimFloatNotationsInternalB.
+Notation "- x" := (opp x) : float_scope.
+Notation "x =? y" := (eqb x y) (at level 70, no associativity) : float_scope.
+Notation "x <? y" := (ltb x y) (at level 70, no associativity) : float_scope.
+Notation "x <=? y" := (leb x y) (at level 70, no associativity) : float_scope.
+Notation "x ?= y" := (compare x y) (at level 70, no associativity) : float_scope.
+Notation "x * y" := (mul x y) : float_scope.
+Notation "x + y" := (add x y) : float_scope.
+Notation "x - y" := (sub x y) : float_scope.
 Notation "x / y" := (div x y) : float_scope.
+End PrimFloatNotationsInternalB.
 
 (** ** Conversions *)
 
@@ -114,15 +119,27 @@ Definition neg_zero := Eval compute in (-zero)%float.
 Definition two := Eval compute in (of_int63 2).
 
 (** ** Predicates and helper functions *)
-Definition is_nan f := negb (f == f)%float.
+Definition is_nan f := negb (f =? f)%float.
 
-Definition is_zero f := (f == zero)%float. (* note: 0 == -0 with floats *)
+Definition is_zero f := (f =? zero)%float. (* note: 0 =? -0 with floats *)
 
-Definition is_infinity f := (abs f == infinity)%float.
+Definition is_infinity f := (abs f =? infinity)%float.
 
 Definition is_finite (x : float) := negb (is_nan x || is_infinity x).
 
 (** [get_sign]: return [true] for [-] sign, [false] for [+] sign. *)
 Definition get_sign f :=
   let f := if is_zero f then (one / f)%float else f in
-  (f < zero)%float.
+  (f <? zero)%float.
+
+Module Export PrimFloatNotations.
+  Local Open Scope float_scope.
+  #[deprecated(since="8.13",note="use infix <? instead")]
+   Notation "x < y" := (x <? y) (at level 70, no associativity) : float_scope.
+  #[deprecated(since="8.13",note="use infix <=? instead")]
+   Notation "x <= y" := (x <=? y) (at level 70, no associativity) : float_scope.
+  #[deprecated(since="8.13",note="use infix =? instead")]
+   Notation "x == y" := (x =? y) (at level 70, no associativity) : float_scope.
+  Export PrimFloatNotationsInternalA.
+  Export PrimFloatNotationsInternalB.
+End PrimFloatNotations.
-- 
cgit v1.2.3