From cd667e48284dce28cd4c6a41eb1f0e62245eff92 Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre@roux01.fr>
Date: Sat, 2 Sep 2023 18:32:46 +0200
Subject: [PATCH] Remove redundant tests

---
 test-suite/primitive/float/add.v              |  63 --
 test-suite/primitive/float/classify.v         |  20 -
 test-suite/primitive/float/compare.v          | 544 ++++++------------
 test-suite/primitive/float/div.v              |  54 --
 test-suite/primitive/float/double_rounding.v  |  27 -
 test-suite/primitive/float/frexp.v            |  28 -
 test-suite/primitive/float/gen_compare.sh     |  15 +-
 test-suite/primitive/float/ldexp.v            |  10 -
 test-suite/primitive/float/mul.v              |  52 --
 test-suite/primitive/float/next_up_down.v     | 137 -----
 test-suite/primitive/float/normfr_mantissa.v  |  16 -
 test-suite/primitive/float/spec_conv.v        |  46 --
 test-suite/primitive/float/sqrt.v             |  36 +-
 test-suite/primitive/float/sub.v              |  39 --
 .../primitive/float/valid_binary_conv.v       |  46 --
 15 files changed, 174 insertions(+), 959 deletions(-)
 delete mode 100644 test-suite/primitive/float/add.v
 delete mode 100644 test-suite/primitive/float/frexp.v
 delete mode 100644 test-suite/primitive/float/spec_conv.v
 delete mode 100644 test-suite/primitive/float/valid_binary_conv.v

diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
deleted file mode 100644
index 21488c271b27..000000000000
--- a/test-suite/primitive/float/add.v
+++ /dev/null
@@ -1,63 +0,0 @@
-Require Import ZArith Uint63 Floats.
-
-Open Scope float_scope.
-
-Definition two := Eval compute in of_uint63 2%uint63.
-Definition three := Eval compute in of_uint63 3%uint63.
-Definition five := Eval compute in of_uint63 5%uint63.
-
-Check (eq_refl : two + three = five).
-Check (eq_refl five <: two + three = five).
-Check (eq_refl five <<: two + three = five).
-Definition compute1 := Eval compute in two + three.
-Check (eq_refl compute1 : five = five).
-
-Definition huge := Eval compute in Z.ldexp one 1023%Z.
-Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
-
-Check (eq_refl : huge + tiny = huge).
-Check (eq_refl huge <: huge + tiny = huge).
-Check (eq_refl huge <<: huge + tiny = huge).
-Definition compute2 := Eval compute in huge + tiny.
-Check (eq_refl compute2 : huge = huge).
-
-Check (eq_refl : huge + huge = infinity).
-Check (eq_refl infinity <: huge + huge = infinity).
-Check (eq_refl infinity <<: huge + huge = infinity).
-Definition compute3 := Eval compute in huge + huge.
-Check (eq_refl compute3 : infinity = infinity).
-
-Check (eq_refl : one + nan = nan).
-Check (eq_refl nan <: one + nan = nan).
-Check (eq_refl nan <<: one + nan = nan).
-Definition compute4 := Eval compute in one + nan.
-Check (eq_refl compute4 : nan = nan).
-
-Check (eq_refl : infinity + infinity = infinity).
-Check (eq_refl infinity <: infinity + infinity = infinity).
-Check (eq_refl infinity <<: infinity + infinity = infinity).
-Definition compute5 := Eval compute in infinity + infinity.
-Check (eq_refl compute5 : infinity = infinity).
-
-Check (eq_refl : infinity + neg_infinity = nan).
-Check (eq_refl nan <: infinity + neg_infinity = nan).
-Check (eq_refl nan <<: infinity + neg_infinity = nan).
-Definition compute6 := Eval compute in infinity + neg_infinity.
-Check (eq_refl compute6 : nan = nan).
-
-Check (eq_refl : zero + zero = zero).
-Check (eq_refl zero <: zero + zero = zero).
-Check (eq_refl zero <<: zero + zero = zero).
-Check (eq_refl : neg_zero + zero = zero).
-Check (eq_refl zero <: neg_zero + zero = zero).
-Check (eq_refl zero <<: neg_zero + zero = zero).
-Check (eq_refl : neg_zero + neg_zero = neg_zero).
-Check (eq_refl neg_zero <: neg_zero + neg_zero = neg_zero).
-Check (eq_refl neg_zero <<: neg_zero + neg_zero = neg_zero).
-Check (eq_refl : zero + neg_zero = zero).
-Check (eq_refl zero <: zero + neg_zero = zero).
-Check (eq_refl zero <<: zero + neg_zero = zero).
-
-Check (eq_refl : huge + neg_infinity = neg_infinity).
-Check (eq_refl neg_infinity <: huge + neg_infinity = neg_infinity).
-Check (eq_refl neg_infinity <<: huge + neg_infinity = neg_infinity).
diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
index 132a379af06f..b8ecf2c7ee1c 100644
--- a/test-suite/primitive/float/classify.v
+++ b/test-suite/primitive/float/classify.v
@@ -11,23 +11,3 @@ Check (eq_refl : classify neg_zero = NZero).
 Check (eq_refl : classify infinity = PInf).
 Check (eq_refl : classify neg_infinity = NInf).
 Check (eq_refl : classify nan = NaN).
-
-Check (eq_refl PNormal <: classify one = PNormal).
-Check (eq_refl NNormal <: classify (- one)%float = NNormal).
-Check (eq_refl PSubn <: classify epsilon = PSubn).
-Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn).
-Check (eq_refl PZero <: classify zero = PZero).
-Check (eq_refl NZero <: classify neg_zero = NZero).
-Check (eq_refl PInf <: classify infinity = PInf).
-Check (eq_refl NInf <: classify neg_infinity = NInf).
-Check (eq_refl NaN <: classify nan = NaN).
-
-Check (eq_refl PNormal <<: classify one = PNormal).
-Check (eq_refl NNormal <<: classify (- one)%float = NNormal).
-Check (eq_refl PSubn <<: classify epsilon = PSubn).
-Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn).
-Check (eq_refl PZero <<: classify zero = PZero).
-Check (eq_refl NZero <<: classify neg_zero = NZero).
-Check (eq_refl PInf <<: classify infinity = PInf).
-Check (eq_refl NInf <<: classify neg_infinity = NInf).
-Check (eq_refl NaN <<: classify nan = NaN).
diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v
index 0e28b25d76e4..739d4bd96fee 100644
--- a/test-suite/primitive/float/compare.v
+++ b/test-suite/primitive/float/compare.v
@@ -6,380 +6,170 @@ Definition min_denorm := Eval compute in Z.ldexp one (-1074)%Z.
 
 Definition min_norm := Eval compute in Z.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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 FLt <<: - infinity ?= one = FLt).
-Check (eq_refl FGt <<: one ?= - infinity = FGt).
+Check (eq_refl : nan =? nan = false).
+Check (eq_refl : nan =? nan = false).
+
+Check (eq_refl : nan <? nan = false).
+Check (eq_refl : nan <? nan = false).
+
+Check (eq_refl : nan <=? nan = false).
+Check (eq_refl : nan <=? nan = false).
+
+Check (eq_refl : nan ?= nan = FNotComparable).
+Check (eq_refl : nan ?= nan = FNotComparable).
+
+Check (eq_refl : nan =? - nan = false).
+Check (eq_refl : - nan =? nan = false).
+
+Check (eq_refl : nan <? - nan = false).
+Check (eq_refl : - nan <? nan = false).
+
+Check (eq_refl : nan <=? - nan = false).
+Check (eq_refl : - nan <=? nan = false).
+
+Check (eq_refl : nan ?= - nan = FNotComparable).
+Check (eq_refl : - nan ?= nan = FNotComparable).
+
+Check (eq_refl : one =? one = true).
+Check (eq_refl : one =? one = true).
+
+Check (eq_refl : one <? one = false).
+Check (eq_refl : one <? one = false).
+
+Check (eq_refl : one <=? one = true).
+Check (eq_refl : one <=? one = true).
+
+Check (eq_refl : one ?= one = FEq).
+Check (eq_refl : one ?= one = FEq).
+
+Check (eq_refl : zero =? zero = true).
+Check (eq_refl : zero =? zero = true).
+
+Check (eq_refl : zero <? zero = false).
+Check (eq_refl : zero <? zero = false).
+
+Check (eq_refl : zero <=? zero = true).
+Check (eq_refl : zero <=? zero = true).
+
+Check (eq_refl : zero ?= zero = FEq).
+Check (eq_refl : zero ?= zero = FEq).
+
+Check (eq_refl : zero =? - zero = true).
+Check (eq_refl : - zero =? zero = true).
+
+Check (eq_refl : zero <? - zero = false).
+Check (eq_refl : - zero <? zero = false).
+
+Check (eq_refl : zero <=? - zero = true).
+Check (eq_refl : - zero <=? zero = true).
+
+Check (eq_refl : zero ?= - zero = FEq).
+Check (eq_refl : - zero ?= zero = FEq).
+
+Check (eq_refl : - zero =? - zero = true).
+Check (eq_refl : - zero =? - zero = true).
+
+Check (eq_refl : - zero <? - zero = false).
+Check (eq_refl : - zero <? - zero = false).
+
+Check (eq_refl : - zero <=? - zero = true).
+Check (eq_refl : - zero <=? - zero = true).
+
+Check (eq_refl : - zero ?= - zero = FEq).
+Check (eq_refl : - zero ?= - zero = FEq).
+
+Check (eq_refl : infinity =? infinity = true).
+Check (eq_refl : infinity =? infinity = true).
+
+Check (eq_refl : infinity <? infinity = false).
+Check (eq_refl : infinity <? infinity = false).
+
+Check (eq_refl : infinity <=? infinity = true).
+Check (eq_refl : infinity <=? infinity = true).
+
+Check (eq_refl : infinity ?= infinity = FEq).
+Check (eq_refl : infinity ?= infinity = FEq).
+
+Check (eq_refl : - infinity =? - infinity = true).
+Check (eq_refl : - infinity =? - infinity = true).
+
+Check (eq_refl : - infinity <? - infinity = false).
+Check (eq_refl : - infinity <? - infinity = false).
+
+Check (eq_refl : - infinity <=? - infinity = true).
+Check (eq_refl : - infinity <=? - infinity = true).
+
+Check (eq_refl : - infinity ?= - infinity = FEq).
+Check (eq_refl : - infinity ?= - infinity = FEq).
+
+Check (eq_refl : min_denorm =? min_norm = false).
+Check (eq_refl : min_norm =? min_denorm = false).
+
+Check (eq_refl : min_denorm <? min_norm = true).
+Check (eq_refl : min_norm <? min_denorm = false).
+
+Check (eq_refl : min_denorm <=? min_norm = true).
+Check (eq_refl : min_norm <=? min_denorm = false).
+
+Check (eq_refl : min_denorm ?= min_norm = FLt).
+Check (eq_refl : min_norm ?= min_denorm = FGt).
+
+Check (eq_refl : min_denorm =? one = false).
+Check (eq_refl : one =? min_denorm = false).
+
+Check (eq_refl : min_denorm <? one = true).
+Check (eq_refl : one <? min_denorm = false).
+
+Check (eq_refl : min_denorm <=? one = true).
+Check (eq_refl : one <=? min_denorm = false).
+
+Check (eq_refl : min_denorm ?= one = FLt).
+Check (eq_refl : one ?= min_denorm = FGt).
+
+Check (eq_refl : min_norm =? one = false).
+Check (eq_refl : one =? min_norm = false).
+
+Check (eq_refl : min_norm <? one = true).
+Check (eq_refl : one <? min_norm = false).
+
+Check (eq_refl : min_norm <=? one = true).
+Check (eq_refl : one <=? min_norm = false).
+
+Check (eq_refl : min_norm ?= one = FLt).
+Check (eq_refl : one ?= min_norm = FGt).
+
+Check (eq_refl : one =? infinity = false).
+Check (eq_refl : infinity =? one = false).
+
+Check (eq_refl : one <? infinity = true).
+Check (eq_refl : infinity <? one = false).
+
+Check (eq_refl : one <=? infinity = true).
+Check (eq_refl : infinity <=? one = false).
+
+Check (eq_refl : one ?= infinity = FLt).
+Check (eq_refl : infinity ?= one = FGt).
+
+Check (eq_refl : - infinity =? infinity = false).
+Check (eq_refl : infinity =? - infinity = false).
+
+Check (eq_refl : - infinity <? infinity = true).
+Check (eq_refl : infinity <? - infinity = false).
+
+Check (eq_refl : - infinity <=? infinity = true).
+Check (eq_refl : infinity <=? - infinity = false).
+
+Check (eq_refl : - infinity ?= infinity = FLt).
+Check (eq_refl : infinity ?= - infinity = FGt).
+
+Check (eq_refl : - infinity =? one = false).
+Check (eq_refl : one =? - infinity = false).
+
+Check (eq_refl : - infinity <? one = true).
+Check (eq_refl : one <? - infinity = false).
+
+Check (eq_refl : - infinity <=? one = true).
+Check (eq_refl : one <=? - infinity = false).
+
+Check (eq_refl : - infinity ?= one = FLt).
+Check (eq_refl : one ?= - infinity = FGt).
diff --git a/test-suite/primitive/float/div.v b/test-suite/primitive/float/div.v
index f2f464255be1..d8e3a8033a09 100644
--- a/test-suite/primitive/float/div.v
+++ b/test-suite/primitive/float/div.v
@@ -2,86 +2,32 @@ Require Import ZArith Uint63 Floats.
 
 Open Scope float_scope.
 
-Definition two := Eval compute in of_uint63 2%uint63.
-Definition three := Eval compute in of_uint63 3%uint63.
-Definition six := Eval compute in of_uint63 6%uint63.
-
-Check (eq_refl : six / three = two).
-Check (eq_refl two <: six / three = two).
-Check (eq_refl two <<: six / three = two).
-Definition compute1 := Eval compute in six / three.
-Check (eq_refl compute1 : two = two).
-
 Definition huge := Eval compute in Z.ldexp one 1023%Z.
 Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
 
 Check (eq_refl : huge / tiny = infinity).
-Check (eq_refl infinity <: huge / tiny = infinity).
-Check (eq_refl infinity <<: huge / tiny = infinity).
-Definition compute2 := Eval compute in huge / tiny.
-Check (eq_refl compute2 : infinity = infinity).
 
 Check (eq_refl : huge / huge = one).
-Check (eq_refl one <: huge / huge = one).
-Check (eq_refl one <<: huge / huge = one).
-Definition compute3 := Eval compute in huge / huge.
-Check (eq_refl compute3 : one = one).
 
 Check (eq_refl : one / nan = nan).
-Check (eq_refl nan <: one / nan = nan).
-Check (eq_refl nan <<: one / nan = nan).
-Definition compute4 := Eval compute in one / nan.
-Check (eq_refl compute4 : nan = nan).
 
 Check (eq_refl : infinity / infinity = nan).
-Check (eq_refl nan <: infinity / infinity = nan).
-Check (eq_refl nan <<: infinity / infinity = nan).
-Definition compute5 := Eval compute in infinity / infinity.
-Check (eq_refl compute5 : nan = nan).
 
 Check (eq_refl : infinity / neg_infinity = nan).
-Check (eq_refl nan <: infinity / neg_infinity = nan).
-Check (eq_refl nan <<: infinity / neg_infinity = nan).
-Definition compute6 := Eval compute in infinity / neg_infinity.
-Check (eq_refl compute6 : nan = nan).
 
 Check (eq_refl : zero / zero = nan).
-Check (eq_refl nan <: zero / zero = nan).
-Check (eq_refl nan <<: zero / zero = nan).
 Check (eq_refl : neg_zero / zero = nan).
-Check (eq_refl nan <: neg_zero / zero = nan).
-Check (eq_refl nan <<: neg_zero / zero = nan).
 
 Check (eq_refl : huge / neg_infinity = neg_zero).
-Check (eq_refl neg_zero <: huge / neg_infinity = neg_zero).
-Check (eq_refl neg_zero <<: huge / neg_infinity = neg_zero).
 
 Check (eq_refl : one / tiny = huge).
-Check (eq_refl huge <: one / tiny = huge).
-Check (eq_refl huge <<: one / tiny = huge).
 Check (eq_refl : one / huge = tiny).
-Check (eq_refl tiny <: one / huge = tiny).
-Check (eq_refl tiny <<: one / huge = tiny).
 Check (eq_refl : zero / huge = zero).
-Check (eq_refl zero <: zero / huge = zero).
-Check (eq_refl zero <<: zero / huge = zero).
 Check (eq_refl : zero / (-huge) = neg_zero).
-Check (eq_refl neg_zero <: zero / (-huge) = neg_zero).
-Check (eq_refl neg_zero <<: zero / (-huge) = neg_zero).
 
 Check (eq_refl : tiny / one = tiny).
-Check (eq_refl tiny <: tiny / one = tiny).
-Check (eq_refl tiny <<: tiny / one = tiny).
 Check (eq_refl : huge / one = huge).
-Check (eq_refl huge <: huge / one = huge).
-Check (eq_refl huge <<: huge / one = huge).
 Check (eq_refl : infinity / one = infinity).
-Check (eq_refl infinity <: infinity / one = infinity).
-Check (eq_refl infinity <<: infinity / one = infinity).
 
 Check (eq_refl : zero / infinity = zero).
-Check (eq_refl zero <: zero / infinity = zero).
-Check (eq_refl zero <<: zero / infinity = zero).
 Check (eq_refl : infinity / zero = infinity).
-Check (eq_refl infinity <: infinity / zero = infinity).
-Check (eq_refl infinity <<: infinity / zero = infinity).
diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v
index 91a7ed9972f8..6bd37cfb8df0 100644
--- a/test-suite/primitive/float/double_rounding.v
+++ b/test-suite/primitive/float/double_rounding.v
@@ -2,24 +2,6 @@ Require Import Floats ZArith.
 
 (* This test check that there is no double rounding with 80 bits registers inside float computations *)
 
-Definition big_cbn := Eval cbn in Z.ldexp one (53)%Z.
-Definition small_cbn := Eval cbn in (one + Z.ldexp one (-52)%Z)%float.
-Definition result_cbn := Eval cbn in (big_cbn + small_cbn)%float.
-Definition check_cbn := Eval cbn in (big_cbn + one)%float.
-
-Check (eq_refl : (result_cbn ?= big_cbn)%float = FGt).
-Check (eq_refl : (check_cbn ?= big_cbn)%float = FEq).
-
-
-Definition big_cbv := Eval cbv in Z.ldexp one (53)%Z.
-Definition small_cbv := Eval cbv in (one + Z.ldexp one (-52)%Z)%float.
-Definition result_cbv := Eval cbv in (big_cbv + small_cbv)%float.
-Definition check_cbv := Eval cbv in (big_cbv + one)%float.
-
-Check (eq_refl : (result_cbv ?= big_cbv)%float = FGt).
-Check (eq_refl : (check_cbv ?= big_cbv)%float = FEq).
-
-
 Definition big_vm := Eval vm_compute in Z.ldexp one (53)%Z.
 Definition small_vm := Eval vm_compute in (one + Z.ldexp one (-52)%Z)%float.
 Definition result_vm := Eval vm_compute in (big_vm + small_vm)%float.
@@ -27,12 +9,3 @@ Definition check_vm := Eval vm_compute in (big_vm + one)%float.
 
 Check (eq_refl : (result_vm ?= big_vm)%float = FGt).
 Check (eq_refl : (check_vm ?= big_vm)%float = FEq).
-
-
-Definition big_native := Eval native_compute in Z.ldexp one (53)%Z.
-Definition small_native := Eval native_compute in (one + Z.ldexp one (-52)%Z)%float.
-Definition result_native := Eval native_compute in (big_native + small_native)%float.
-Definition check_native := Eval native_compute in (big_native + one)%float.
-
-Check (eq_refl : (result_native ?= big_native)%float = FGt).
-Check (eq_refl : (check_native ?= big_native)%float = FEq).
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
deleted file mode 100644
index fde12ab3f5dd..000000000000
--- a/test-suite/primitive/float/frexp.v
+++ /dev/null
@@ -1,28 +0,0 @@
-Require Import ZArith Floats.
-
-Definition denorm := Eval compute in Z.ldexp one (-1074)%Z.
-Definition neg_one := Eval compute in (-one)%float.
-
-Check (eq_refl : let (m,e) := Z.frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <: let (m,e) := Z.frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <<: let (m,e) := Z.frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
-
-Check (eq_refl : let (m,e) := Z.frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <: let (m,e) := Z.frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <<: let (m,e) := Z.frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
-
-Check (eq_refl : let (m,e) := Z.frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <: let (m,e) := Z.frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <<: let (m,e) := Z.frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
-
-Check (eq_refl : let (m,e) := Z.frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <: let (m,e) := Z.frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <<: let (m,e) := Z.frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
-
-Check (eq_refl : let (m,e) := Z.frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <: let (m,e) := Z.frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <<: let (m,e) := Z.frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
-
-Check (eq_refl : let (m,e) := Z.frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <: let (m,e) := Z.frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
-Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <<: let (m,e) := Z.frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh
index 0f7c7ddd5c86..7d0e489f07d1 100755
--- a/test-suite/primitive/float/gen_compare.sh
+++ b/test-suite/primitive/float/gen_compare.sh
@@ -19,20 +19,17 @@ genTest() {
     if [ $# -ne 10 ]; then
         echo >&2 "genTest expects 10 arguments"
     fi
-    TACTICS=(":" "<:" "<<:")
     OPS=("=?" "<?" "<=?" "?=")
     x="$1"
     y="$2"
     OPS1=("$3" "$4" "$5" "$6")  # for x y
     OPS2=("$7" "$8" "$9" "${10}") # for y x
-    for tac in "${TACTICS[@]}"; do
-        for i in {0..3}; do
-            op="${OPS[$i]}"
-            op1="${OPS1[$i]}"
-            op2="${OPS2[$i]}"
-            echo "Check (eq_refl $op1 $tac $x $op $y = $op1)."
-            echo "Check (eq_refl $op2 $tac $y $op $x = $op2)."
-        done
+    for i in {0..3}; do
+        op="${OPS[$i]}"
+        op1="${OPS1[$i]}"
+        op2="${OPS2[$i]}"
+        echo "Check (eq_refl : $x $op $y = $op1)."
+        echo "Check (eq_refl : $y $op $x = $op2)."
         echo
     done
 }
diff --git a/test-suite/primitive/float/ldexp.v b/test-suite/primitive/float/ldexp.v
index 599df7e8d9f7..b55af10ea8f5 100644
--- a/test-suite/primitive/float/ldexp.v
+++ b/test-suite/primitive/float/ldexp.v
@@ -1,21 +1,11 @@
 Require Import ZArith Uint63 Floats.
 
 Check (eq_refl : Z.ldexp one 9223372036854773807%Z = infinity).
-Check (eq_refl infinity <: Z.ldexp one 9223372036854773807%Z = infinity).
-Check (eq_refl infinity <<: Z.ldexp one 9223372036854773807%Z = infinity).
 
 Check (eq_refl : ldshiftexp one 9223372036854775807 = infinity).
-Check (eq_refl infinity <: ldshiftexp one 9223372036854775807 = infinity).
-Check (eq_refl infinity <<: ldshiftexp one 9223372036854775807 = infinity).
 
 Check (eq_refl : Z.ldexp one (-2102) = 0%float).
-Check (eq_refl 0%float <: Z.ldexp one (-2102) = 0%float).
-Check (eq_refl 0%float <<: Z.ldexp one (-2102) = 0%float).
 
 Check (eq_refl : Z.ldexp one (-3) = 0.125%float).
-Check (eq_refl 0.125%float <: Z.ldexp one (-3) = 0.125%float).
-Check (eq_refl 0.125%float <<: Z.ldexp one (-3) = 0.125%float).
 
 Check (eq_refl : Z.ldexp one 3 = 8%float).
-Check (eq_refl 8%float <: Z.ldexp one 3 = 8%float).
-Check (eq_refl 8%float <<: Z.ldexp one 3 = 8%float).
diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v
index ec0af531aa92..bb7d87fd3e69 100644
--- a/test-suite/primitive/float/mul.v
+++ b/test-suite/primitive/float/mul.v
@@ -2,82 +2,30 @@ Require Import ZArith Uint63 Floats.
 
 Open Scope float_scope.
 
-Definition two := Eval compute in of_uint63 2%uint63.
-Definition three := Eval compute in of_uint63 3%uint63.
-Definition six := Eval compute in of_uint63 6%uint63.
-
-Check (eq_refl : three * two = six).
-Check (eq_refl six <: three * two = six).
-Check (eq_refl six <<: three * two = six).
-Definition compute1 := Eval compute in three * two.
-Check (eq_refl compute1 : six = six).
-
 Definition huge := Eval compute in Z.ldexp one 1023%Z.
 Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
 
 Check (eq_refl : huge * tiny = one).
-Check (eq_refl one <: huge * tiny = one).
-Check (eq_refl one <<: huge * tiny = one).
-Definition compute2 := Eval compute in huge * tiny.
-Check (eq_refl compute2 : one = one).
 
 Check (eq_refl : huge * huge = infinity).
-Check (eq_refl infinity <: huge * huge = infinity).
-Check (eq_refl infinity <<: huge * huge = infinity).
-Definition compute3 := Eval compute in huge * huge.
-Check (eq_refl compute3 : infinity = infinity).
 
 Check (eq_refl : one * nan = nan).
-Check (eq_refl nan <: one * nan = nan).
-Check (eq_refl nan <<: one * nan = nan).
-Definition compute4 := Eval compute in one * nan.
-Check (eq_refl compute4 : nan = nan).
 
 Check (eq_refl : infinity * infinity = infinity).
-Check (eq_refl infinity <: infinity * infinity = infinity).
-Check (eq_refl infinity <<: infinity * infinity = infinity).
-Definition compute5 := Eval compute in infinity * infinity.
-Check (eq_refl compute5 : infinity = infinity).
 
 Check (eq_refl : infinity * neg_infinity = neg_infinity).
-Check (eq_refl neg_infinity <: infinity * neg_infinity = neg_infinity).
-Check (eq_refl neg_infinity <<: infinity * neg_infinity = neg_infinity).
-Definition compute6 := Eval compute in infinity * neg_infinity.
-Check (eq_refl compute6 : neg_infinity = neg_infinity).
 
 Check (eq_refl : zero * zero = zero).
-Check (eq_refl zero <: zero * zero = zero).
-Check (eq_refl zero <<: zero * zero = zero).
 Check (eq_refl : neg_zero * zero = neg_zero).
-Check (eq_refl neg_zero <: neg_zero * zero = neg_zero).
-Check (eq_refl neg_zero <<: neg_zero * zero = neg_zero).
 Check (eq_refl : neg_zero * neg_zero = zero).
-Check (eq_refl zero <: neg_zero * neg_zero = zero).
-Check (eq_refl zero <<: neg_zero * neg_zero = zero).
 Check (eq_refl : zero * neg_zero = neg_zero).
-Check (eq_refl neg_zero <: zero * neg_zero = neg_zero).
-Check (eq_refl neg_zero <<: zero * neg_zero = neg_zero).
 
 Check (eq_refl : huge * neg_infinity = neg_infinity).
-Check (eq_refl neg_infinity <: huge * neg_infinity = neg_infinity).
-Check (eq_refl neg_infinity <<: huge * neg_infinity = neg_infinity).
 
 Check (eq_refl : one * tiny = tiny).
-Check (eq_refl tiny <: one * tiny = tiny).
-Check (eq_refl tiny <<: one * tiny = tiny).
 Check (eq_refl : one * huge = huge).
-Check (eq_refl huge <: one * huge = huge).
-Check (eq_refl huge <<: one * huge = huge).
 Check (eq_refl : zero * huge = zero).
-Check (eq_refl zero <: zero * huge = zero).
-Check (eq_refl zero <<: zero * huge = zero).
 Check (eq_refl : zero * (-huge) = neg_zero).
-Check (eq_refl neg_zero <: zero * (-huge) = neg_zero).
-Check (eq_refl neg_zero <<: zero * (-huge) = neg_zero).
 
 Check (eq_refl : zero * infinity = nan).
-Check (eq_refl nan <: zero * infinity = nan).
-Check (eq_refl nan <<: zero * infinity = nan).
 Check (eq_refl : neg_infinity * zero = nan).
-Check (eq_refl nan <: neg_infinity * zero = nan).
-Check (eq_refl nan <<: neg_infinity * zero = nan).
diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v
index df8a9dbad41a..cc51aeef66f5 100644
--- a/test-suite/primitive/float/next_up_down.v
+++ b/test-suite/primitive/float/next_up_down.v
@@ -2,125 +2,6 @@ Require Import ZArith Uint63 Floats.
 
 Open Scope float_scope.
 
-Definition f0 := zero.
-Definition f1 := neg_zero.
-Definition f2 := Eval compute in Z.ldexp one 0.
-Definition f3 := Eval compute in -f1.
-(* smallest positive float *)
-Definition f4 := Eval compute in Z.ldexp one (-1074).
-Definition f5 := Eval compute in -f3.
-Definition f6 := infinity.
-Definition f7 := neg_infinity.
-Definition f8 := Eval compute in Z.ldexp one (-1).
-Definition f9 := Eval compute in -f8.
-Definition f10 := Eval compute in of_uint63 42.
-Definition f11 := Eval compute in -f10.
-(* max float *)
-Definition f12 := Eval compute in Z.ldexp (of_uint63 9007199254740991) 1024.
-Definition f13 := Eval compute in -f12.
-(* smallest positive normalized float *)
-Definition f14 := Eval compute in Z.ldexp one (-1022).
-Definition f15 := Eval compute in -f14.
-
-Check (eq_refl : Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
-Check (eq_refl : Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
-Check (eq_refl : Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
-Check (eq_refl : Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
-Check (eq_refl : Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
-Check (eq_refl : Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
-Check (eq_refl : Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
-Check (eq_refl : Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
-Check (eq_refl : Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
-Check (eq_refl : Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
-Check (eq_refl : Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
-Check (eq_refl : Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
-Check (eq_refl : Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
-Check (eq_refl : Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
-Check (eq_refl : Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
-Check (eq_refl : Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
-Check (eq_refl : Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
-Check (eq_refl : Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
-Check (eq_refl : Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
-Check (eq_refl : Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
-Check (eq_refl : Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
-Check (eq_refl : Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
-Check (eq_refl : Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
-Check (eq_refl : Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
-Check (eq_refl : Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
-Check (eq_refl : Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
-Check (eq_refl : Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
-Check (eq_refl : Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
-Check (eq_refl : Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
-Check (eq_refl : Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
-Check (eq_refl : Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
-Check (eq_refl : Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
-
-Check (eq_refl (SF64succ (Prim2SF f0)) <: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
-Check (eq_refl (SF64pred (Prim2SF f0)) <: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
-Check (eq_refl (SF64succ (Prim2SF f1)) <: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
-Check (eq_refl (SF64pred (Prim2SF f1)) <: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
-Check (eq_refl (SF64succ (Prim2SF f2)) <: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
-Check (eq_refl (SF64pred (Prim2SF f2)) <: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
-Check (eq_refl (SF64succ (Prim2SF f3)) <: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
-Check (eq_refl (SF64pred (Prim2SF f3)) <: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
-Check (eq_refl (SF64succ (Prim2SF f4)) <: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
-Check (eq_refl (SF64pred (Prim2SF f4)) <: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
-Check (eq_refl (SF64succ (Prim2SF f5)) <: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
-Check (eq_refl (SF64pred (Prim2SF f5)) <: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
-Check (eq_refl (SF64succ (Prim2SF f6)) <: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
-Check (eq_refl (SF64pred (Prim2SF f6)) <: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
-Check (eq_refl (SF64succ (Prim2SF f7)) <: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
-Check (eq_refl (SF64pred (Prim2SF f7)) <: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
-Check (eq_refl (SF64succ (Prim2SF f8)) <: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
-Check (eq_refl (SF64pred (Prim2SF f8)) <: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
-Check (eq_refl (SF64succ (Prim2SF f9)) <: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
-Check (eq_refl (SF64pred (Prim2SF f9)) <: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
-Check (eq_refl (SF64succ (Prim2SF f10)) <: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
-Check (eq_refl (SF64pred (Prim2SF f10)) <: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
-Check (eq_refl (SF64succ (Prim2SF f11)) <: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
-Check (eq_refl (SF64pred (Prim2SF f11)) <: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
-Check (eq_refl (SF64succ (Prim2SF f12)) <: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
-Check (eq_refl (SF64pred (Prim2SF f12)) <: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
-Check (eq_refl (SF64succ (Prim2SF f13)) <: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
-Check (eq_refl (SF64pred (Prim2SF f13)) <: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
-Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
-Check (eq_refl (SF64pred (Prim2SF f14)) <: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
-Check (eq_refl (SF64succ (Prim2SF f15)) <: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
-Check (eq_refl (SF64pred (Prim2SF f15)) <: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
-
-Check (eq_refl (SF64succ (Prim2SF f0)) <<: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
-Check (eq_refl (SF64pred (Prim2SF f0)) <<: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
-Check (eq_refl (SF64succ (Prim2SF f1)) <<: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
-Check (eq_refl (SF64pred (Prim2SF f1)) <<: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
-Check (eq_refl (SF64succ (Prim2SF f2)) <<: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
-Check (eq_refl (SF64pred (Prim2SF f2)) <<: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
-Check (eq_refl (SF64succ (Prim2SF f3)) <<: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
-Check (eq_refl (SF64pred (Prim2SF f3)) <<: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
-Check (eq_refl (SF64succ (Prim2SF f4)) <<: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
-Check (eq_refl (SF64pred (Prim2SF f4)) <<: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
-Check (eq_refl (SF64succ (Prim2SF f5)) <<: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
-Check (eq_refl (SF64pred (Prim2SF f5)) <<: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
-Check (eq_refl (SF64succ (Prim2SF f6)) <<: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
-Check (eq_refl (SF64pred (Prim2SF f6)) <<: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
-Check (eq_refl (SF64succ (Prim2SF f7)) <<: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
-Check (eq_refl (SF64pred (Prim2SF f7)) <<: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
-Check (eq_refl (SF64succ (Prim2SF f8)) <<: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
-Check (eq_refl (SF64pred (Prim2SF f8)) <<: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
-Check (eq_refl (SF64succ (Prim2SF f9)) <<: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
-Check (eq_refl (SF64pred (Prim2SF f9)) <<: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
-Check (eq_refl (SF64succ (Prim2SF f10)) <<: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
-Check (eq_refl (SF64pred (Prim2SF f10)) <<: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
-Check (eq_refl (SF64succ (Prim2SF f11)) <<: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
-Check (eq_refl (SF64pred (Prim2SF f11)) <<: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
-Check (eq_refl (SF64succ (Prim2SF f12)) <<: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
-Check (eq_refl (SF64pred (Prim2SF f12)) <<: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
-Check (eq_refl (SF64succ (Prim2SF f13)) <<: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
-Check (eq_refl (SF64pred (Prim2SF f13)) <<: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
-Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
-Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
-Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
-Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
-
 Check (eq_refl : next_up nan = nan).
 Check (eq_refl : next_down nan = nan).
 Check (eq_refl : next_up neg_infinity = -0x1.fffffffffffffp+1023).
@@ -133,32 +14,14 @@ Check (eq_refl : next_up (-0x1.fffffffffffff) = -0x1.ffffffffffffe).
 Check (eq_refl : next_down (-0x1.fffffffffffff) = -0x1p+1).
 Check (eq_refl : next_up (-0x1p1) = -0x1.fffffffffffff).
 Check (eq_refl : next_down (-0x1p1) = -0x1.0000000000001p+1).
-Check (eq_refl : next_up (-0x1p-1022) = -0x0.fffffffffffffp-1022).
-Check (eq_refl : next_down (-0x1p-1022) = -0x1.0000000000001p-1022).
-Check (eq_refl : next_up (-0x0.fffffffffffffp-1022) = -0x0.ffffffffffffep-1022).
-Check (eq_refl : next_down (-0x0.fffffffffffffp-1022) = -0x1p-1022).
-Check (eq_refl : next_up (-0x0.01p-1022) = -0x0.00fffffffffffp-1022).
-Check (eq_refl : next_down (-0x0.01p-1022) = -0x0.0100000000001p-1022).
-Check (eq_refl : next_up (-0x0.0000000000001p-1022) = -0).
-Check (eq_refl : next_down (-0x0.0000000000001p-1022) = -0x0.0000000000002p-1022).
 Check (eq_refl : next_up (-0) = 0x0.0000000000001p-1022).
 Check (eq_refl : next_down (-0) = -0x0.0000000000001p-1022).
 Check (eq_refl : next_up 0 = 0x0.0000000000001p-1022).
 Check (eq_refl : next_down 0 = -0x0.0000000000001p-1022).
-Check (eq_refl : next_up 0x0.0000000000001p-1022 = 0x0.0000000000002p-1022).
-Check (eq_refl : next_down 0x0.0000000000001p-1022 = 0).
-Check (eq_refl : next_up 0x0.01p-1022 = 0x0.0100000000001p-1022).
-Check (eq_refl : next_down 0x0.01p-1022 = 0x0.00fffffffffffp-1022).
-Check (eq_refl : next_up 0x0.fffffffffffffp-1022 = 0x1p-1022).
-Check (eq_refl : next_down 0x0.fffffffffffffp-1022 = 0x0.ffffffffffffep-1022).
-Check (eq_refl : next_up 0x1p-1022 = 0x1.0000000000001p-1022).
-Check (eq_refl : next_down 0x1p-1022 = 0x0.fffffffffffffp-1022).
 Check (eq_refl : next_up 0x1p1 = 0x1.0000000000001p+1).
 Check (eq_refl : next_down 0x1p1 = 0x1.fffffffffffff).
 Check (eq_refl : next_up 0x1.fffffffffffff = 0x1p+1).
 Check (eq_refl : next_down 0x1.fffffffffffff = 0x1.ffffffffffffe).
-Check (eq_refl : next_up 0x1.ffffffffffffap+1023 = 0x1.ffffffffffffbp+1023).
-Check (eq_refl : next_down 0x1.ffffffffffffap+1023 = 0x1.ffffffffffff9p+1023).
 Check (eq_refl : next_up 0x1.fffffffffffffp+1023 = infinity).
 Check (eq_refl : next_down 0x1.fffffffffffffp+1023 = 0x1.ffffffffffffep+1023).
 Check (eq_refl : next_up infinity = infinity).
diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v
index 826cf1c5801d..35bf20adc0b0 100644
--- a/test-suite/primitive/float/normfr_mantissa.v
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -10,19 +10,3 @@ Check (eq_refl : normfr_mantissa (-one) = 0%uint63).
 Check (eq_refl : normfr_mantissa zero = 0%uint63).
 Check (eq_refl : normfr_mantissa nan = 0%uint63).
 Check (eq_refl : normfr_mantissa three_quarters = (3 << 51)%uint63).
-
-Check (eq_refl 0%uint63 <: normfr_mantissa one = 0%uint63).
-Check (eq_refl (1 << 52)%uint63 <: normfr_mantissa half = (1 << 52)%uint63).
-Check (eq_refl (1 << 52)%uint63 <: normfr_mantissa (-half) = (1 << 52)%uint63).
-Check (eq_refl 0%uint63 <: normfr_mantissa (-one) = 0%uint63).
-Check (eq_refl 0%uint63 <: normfr_mantissa zero = 0%uint63).
-Check (eq_refl 0%uint63 <: normfr_mantissa nan = 0%uint63).
-Check (eq_refl (3 << 51)%uint63 <: normfr_mantissa three_quarters = (3 << 51)%uint63).
-
-Check (eq_refl 0%uint63 <<: normfr_mantissa one = 0%uint63).
-Check (eq_refl (1 << 52)%uint63 <<: normfr_mantissa half = (1 << 52)%uint63).
-Check (eq_refl (1 << 52)%uint63 <<: normfr_mantissa (-half) = (1 << 52)%uint63).
-Check (eq_refl 0%uint63 <<: normfr_mantissa (-one) = 0%uint63).
-Check (eq_refl 0%uint63 <<: normfr_mantissa zero = 0%uint63).
-Check (eq_refl 0%uint63 <<: normfr_mantissa nan = 0%uint63).
-Check (eq_refl (3 << 51)%uint63 <<: normfr_mantissa three_quarters = (3 << 51)%uint63).
diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v
deleted file mode 100644
index 80c64c4c4f08..000000000000
--- a/test-suite/primitive/float/spec_conv.v
+++ /dev/null
@@ -1,46 +0,0 @@
-Require Import ZArith Floats.
-
-Definition two := Eval compute in (one + one)%float.
-Definition half := Eval compute in (one / two)%float.
-Definition huge := Eval compute in Z.ldexp one (1023)%Z.
-Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
-Definition denorm := Eval compute in Z.ldexp one (-1074)%Z.
-
-Check (eq_refl : SF2Prim (Prim2SF zero) = zero).
-Check (eq_refl : SF2Prim (Prim2SF neg_zero) = neg_zero).
-Check (eq_refl : SF2Prim (Prim2SF one) = one).
-Check (eq_refl : SF2Prim (Prim2SF (-one)) = (-one)%float).
-Check (eq_refl : SF2Prim (Prim2SF infinity) = infinity).
-Check (eq_refl : SF2Prim (Prim2SF neg_infinity) = neg_infinity).
-Check (eq_refl : SF2Prim (Prim2SF huge) = huge).
-Check (eq_refl : SF2Prim (Prim2SF tiny) = tiny).
-Check (eq_refl : SF2Prim (Prim2SF denorm) = denorm).
-Check (eq_refl : SF2Prim (Prim2SF nan) = nan).
-Check (eq_refl : SF2Prim (Prim2SF two) = two).
-Check (eq_refl : SF2Prim (Prim2SF half) = half).
-
-Check (eq_refl zero <: SF2Prim (Prim2SF zero) = zero).
-Check (eq_refl neg_zero <: SF2Prim (Prim2SF neg_zero) = neg_zero).
-Check (eq_refl one <: SF2Prim (Prim2SF one) = one).
-Check (eq_refl (-one)%float <: SF2Prim (Prim2SF (-one)) = (-one)%float).
-Check (eq_refl infinity <: SF2Prim (Prim2SF infinity) = infinity).
-Check (eq_refl neg_infinity <: SF2Prim (Prim2SF neg_infinity) = neg_infinity).
-Check (eq_refl huge <: SF2Prim (Prim2SF huge) = huge).
-Check (eq_refl tiny <: SF2Prim (Prim2SF tiny) = tiny).
-Check (eq_refl denorm <: SF2Prim (Prim2SF denorm) = denorm).
-Check (eq_refl nan <: SF2Prim (Prim2SF nan) = nan).
-Check (eq_refl two <: SF2Prim (Prim2SF two) = two).
-Check (eq_refl half <: SF2Prim (Prim2SF half) = half).
-
-Check (eq_refl zero <<: SF2Prim (Prim2SF zero) = zero).
-Check (eq_refl neg_zero <<: SF2Prim (Prim2SF neg_zero) = neg_zero).
-Check (eq_refl one <<: SF2Prim (Prim2SF one) = one).
-Check (eq_refl (-one)%float <<: SF2Prim (Prim2SF (-one)) = (-one)%float).
-Check (eq_refl infinity <<: SF2Prim (Prim2SF infinity) = infinity).
-Check (eq_refl neg_infinity <<: SF2Prim (Prim2SF neg_infinity) = neg_infinity).
-Check (eq_refl huge <<: SF2Prim (Prim2SF huge) = huge).
-Check (eq_refl tiny <<: SF2Prim (Prim2SF tiny) = tiny).
-Check (eq_refl denorm <<: SF2Prim (Prim2SF denorm) = denorm).
-Check (eq_refl nan <<: SF2Prim (Prim2SF nan) = nan).
-Check (eq_refl two <<: SF2Prim (Prim2SF two) = two).
-Check (eq_refl half <<: SF2Prim (Prim2SF half) = half).
diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v
index a6ab8659e080..01f9fee92570 100644
--- a/test-suite/primitive/float/sqrt.v
+++ b/test-suite/primitive/float/sqrt.v
@@ -6,44 +6,10 @@ Definition three := Eval compute in of_uint63 3%uint63.
 Definition nine := Eval compute in of_uint63 9%uint63.
 
 Check (eq_refl : sqrt nine = three).
-Check (eq_refl three <: sqrt nine = three).
-Definition compute1 := Eval compute in sqrt nine.
-Check (eq_refl : three = three).
 
-Definition huge := Eval compute in Z.ldexp one (1023)%Z.
-Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
-Definition denorm := Eval compute in Z.ldexp one (-1074)%Z.
-
-Goal (Prim2SF (sqrt huge) = SF64sqrt (Prim2SF huge)).
-  now compute. Undo. now vm_compute.
-Qed.
-
-Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)).
-  now compute. Undo. now vm_compute.
-Qed.
-
-Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)).
-  now compute. Undo. now vm_compute.
-Qed.
-
-Check (eq_refl : sqrt neg_zero = neg_zero).
-Check (eq_refl neg_zero <: sqrt neg_zero = neg_zero).
-Check (eq_refl neg_zero <<: sqrt neg_zero = neg_zero).
 Check (eq_refl : sqrt zero = zero).
-Check (eq_refl zero <: sqrt zero = zero).
-Check (eq_refl zero <<: sqrt zero = zero).
+Check (eq_refl : sqrt neg_zero = neg_zero).
 Check (eq_refl : sqrt one = one).
-Check (eq_refl one <: sqrt one = one).
-Check (eq_refl one <<: sqrt one = one).
 Check (eq_refl : sqrt (-one) = nan).
-Check (eq_refl nan <: sqrt (-one) = nan).
-Check (eq_refl nan <<: sqrt (-one) = nan).
 Check (eq_refl : sqrt infinity = infinity).
-Check (eq_refl infinity <: sqrt infinity = infinity).
-Check (eq_refl infinity <<: sqrt infinity = infinity).
 Check (eq_refl : sqrt neg_infinity = nan).
-Check (eq_refl nan <: sqrt neg_infinity = nan).
-Check (eq_refl nan <<: sqrt neg_infinity = nan).
-Check (eq_refl : sqrt infinity = infinity).
-Check (eq_refl infinity <: sqrt infinity = infinity).
-Check (eq_refl infinity <<: sqrt infinity = infinity).
diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v
index 3b1e21bf4913..2a6b73b3081b 100644
--- a/test-suite/primitive/float/sub.v
+++ b/test-suite/primitive/float/sub.v
@@ -2,61 +2,22 @@ Require Import ZArith Uint63 Floats.
 
 Open Scope float_scope.
 
-Definition two := Eval compute in of_uint63 2%uint63.
-Definition three := Eval compute in of_uint63 3%uint63.
-
-Check (eq_refl : three - two = one).
-Check (eq_refl one <: three - two = one).
-Check (eq_refl one <<: three - two = one).
-Definition compute1 := Eval compute in three - two.
-Check (eq_refl compute1 : one = one).
-
 Definition huge := Eval compute in Z.ldexp one 1023%Z.
 Definition tiny := Eval compute in Z.ldexp one (-1023)%Z.
 
 Check (eq_refl : huge - tiny = huge).
-Check (eq_refl huge <: huge - tiny = huge).
-Check (eq_refl huge <<: huge - tiny = huge).
-Definition compute2 := Eval compute in huge - tiny.
-Check (eq_refl compute2 : huge = huge).
 
 Check (eq_refl : huge - huge = zero).
-Check (eq_refl zero <: huge - huge = zero).
-Check (eq_refl zero <<: huge - huge = zero).
-Definition compute3 := Eval compute in huge - huge.
-Check (eq_refl compute3 : zero = zero).
 
 Check (eq_refl : one - nan = nan).
-Check (eq_refl nan <: one - nan = nan).
-Check (eq_refl nan <<: one - nan = nan).
-Definition compute4 := Eval compute in one - nan.
-Check (eq_refl compute4 : nan = nan).
 
 Check (eq_refl : infinity - infinity = nan).
-Check (eq_refl nan <: infinity - infinity = nan).
-Check (eq_refl nan <<: infinity - infinity = nan).
-Definition compute5 := Eval compute in infinity - infinity.
-Check (eq_refl compute5 : nan = nan).
 
 Check (eq_refl : infinity - neg_infinity = infinity).
-Check (eq_refl infinity <: infinity - neg_infinity = infinity).
-Check (eq_refl infinity <<: infinity - neg_infinity = infinity).
-Definition compute6 := Eval compute in infinity - neg_infinity.
-Check (eq_refl compute6 : infinity = infinity).
 
 Check (eq_refl : zero - zero = zero).
-Check (eq_refl zero <: zero - zero = zero).
-Check (eq_refl zero <<: zero - zero = zero).
 Check (eq_refl : neg_zero - zero = neg_zero).
-Check (eq_refl neg_zero <: neg_zero - zero = neg_zero).
-Check (eq_refl neg_zero <<: neg_zero - zero = neg_zero).
 Check (eq_refl : neg_zero - neg_zero = zero).
-Check (eq_refl zero <: neg_zero - neg_zero = zero).
-Check (eq_refl zero <<: neg_zero - neg_zero = zero).
 Check (eq_refl : zero - neg_zero = zero).
-Check (eq_refl zero <: zero - neg_zero = zero).
-Check (eq_refl zero <<: zero - neg_zero = zero).
 
 Check (eq_refl : huge - neg_infinity = infinity).
-Check (eq_refl infinity <: huge - neg_infinity = infinity).
-Check (eq_refl infinity <<: huge - neg_infinity = infinity).
diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v
deleted file mode 100644
index 3cea22e35a2b..000000000000
--- a/test-suite/primitive/float/valid_binary_conv.v
+++ /dev/null
@@ -1,46 +0,0 @@
-Require Import ZArith Floats.
-
-Definition two := Eval compute in (one + one)%float.
-Definition half := Eval compute in (one / two)%float.
-Definition huge := Eval compute in Z.ldexp one (1023)%Z.
-Definition tiny := Eval compute in Z.ldexp one (-1022)%Z.
-Definition denorm := Eval compute in Z.ldexp one (-1074)%Z.
-
-Check (eq_refl : valid_binary (Prim2SF zero) = true).
-Check (eq_refl : valid_binary (Prim2SF neg_zero) = true).
-Check (eq_refl : valid_binary (Prim2SF one) = true).
-Check (eq_refl : valid_binary (Prim2SF (-one)) = true).
-Check (eq_refl : valid_binary (Prim2SF infinity) = true).
-Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true).
-Check (eq_refl : valid_binary (Prim2SF huge) = true).
-Check (eq_refl : valid_binary (Prim2SF tiny) = true).
-Check (eq_refl : valid_binary (Prim2SF denorm) = true).
-Check (eq_refl : valid_binary (Prim2SF nan) = true).
-Check (eq_refl : valid_binary (Prim2SF two) = true).
-Check (eq_refl : valid_binary (Prim2SF half) = true).
-
-Check (eq_refl true <: valid_binary (Prim2SF zero) = true).
-Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true).
-Check (eq_refl true <: valid_binary (Prim2SF one) = true).
-Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true).
-Check (eq_refl true <: valid_binary (Prim2SF infinity) = true).
-Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true).
-Check (eq_refl true <: valid_binary (Prim2SF huge) = true).
-Check (eq_refl true <: valid_binary (Prim2SF tiny) = true).
-Check (eq_refl true <: valid_binary (Prim2SF denorm) = true).
-Check (eq_refl true <: valid_binary (Prim2SF nan) = true).
-Check (eq_refl true <: valid_binary (Prim2SF two) = true).
-Check (eq_refl true <: valid_binary (Prim2SF half) = true).
-
-Check (eq_refl true <<: valid_binary (Prim2SF zero) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF neg_zero) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF one) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF (-one)) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF infinity) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF neg_infinity) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF huge) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF tiny) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF denorm) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF nan) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF two) = true).
-Check (eq_refl true <<: valid_binary (Prim2SF half) = true).