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

3 files changed, 254 insertions, 254 deletions

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