Add tests for primitive floats with 'native_compute'

Tests are updated to include native computations.

12 files changed, 156 insertions, 2 deletions

diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
index 5b15eb2fa7..f8c5939d0a 100644
--- a/test-suite/primitive/float/add.v
+++ b/test-suite/primitive/float/add.v
@@ -8,7 +8,7 @@ Definition five := Eval compute in of_int63 5%int63.
 
 Check (eq_refl : two + three = five).
 Check (eq_refl five <: 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).
 
@@ -17,38 +17,47 @@ Definition tiny := Eval compute in ldexp one (-1023)%Z.
 
 Check (eq_refl : huge + tiny = huge).
 Check (eq_refl huge <: 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 e4373415cb..22e3fca844 100644
--- a/test-suite/primitive/float/classify.v
+++ b/test-suite/primitive/float/classify.v
@@ -21,3 +21,13 @@ 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/div.v b/test-suite/primitive/float/div.v
index 5c231192fd..8e971f575b 100644
--- a/test-suite/primitive/float/div.v
+++ b/test-suite/primitive/float/div.v
@@ -8,6 +8,7 @@ Definition six := Eval compute in of_int63 6%int63.
 
 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).
 
@@ -16,54 +17,71 @@ Definition tiny := Eval compute in 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 8aa9b4ca45..e2356cdd7b 100644
--- a/test-suite/primitive/float/double_rounding.v
+++ b/test-suite/primitive/float/double_rounding.v
@@ -27,3 +27,12 @@ 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 ldexp one (53)%Z.
+Definition small_native := Eval native_compute in (one + 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
index 3a3cbed4e2..2a600429b1 100644
--- a/test-suite/primitive/float/frexp.v
+++ b/test-suite/primitive/float/frexp.v
@@ -5,18 +5,24 @@ Definition neg_one := Eval compute in (-one)%float.
 
 Check (eq_refl : let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
 Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <<: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
 
 Check (eq_refl : let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
 Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <<: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
 
 Check (eq_refl : let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
 Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <<: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
 
 Check (eq_refl : let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
 Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <<: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
 
 Check (eq_refl : let (m,e) := 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) := 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) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
 
 Check (eq_refl : let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
 Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <<: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v
index a335889c05..91fe7e9791 100644
--- a/test-suite/primitive/float/mul.v
+++ b/test-suite/primitive/float/mul.v
@@ -8,6 +8,7 @@ Definition six := Eval compute in of_int63 6%int63.
 
 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).
 
@@ -16,51 +17,67 @@ Definition tiny := Eval compute in 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 95f5248bf7..4f8427dc5b 100644
--- a/test-suite/primitive/float/next_up_down.v
+++ b/test-suite/primitive/float/next_up_down.v
@@ -87,3 +87,36 @@ Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Pri
 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)).
diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v
index e1a465a9e1..28bd1c03f5 100644
--- a/test-suite/primitive/float/normfr_mantissa.v
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -18,3 +18,11 @@ Check (eq_refl 0%int63 <: normfr_mantissa (-one) = 0%int63).
 Check (eq_refl 0%int63 <: normfr_mantissa zero = 0%int63).
 Check (eq_refl 0%int63 <: normfr_mantissa nan = 0%int63).
 Check (eq_refl (3 << 51)%int63 <: normfr_mantissa three_quarters = (3 << 51)%int63).
+
+Check (eq_refl 0%int63 <<: normfr_mantissa one = 0%int63).
+Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa (-one) = 0%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa zero = 0%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa nan = 0%int63).
+Check (eq_refl (3 << 51)%int63 <<: normfr_mantissa three_quarters = (3 << 51)%int63).
diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v
index d7e87275a9..a610d39671 100644
--- a/test-suite/primitive/float/spec_conv.v
+++ b/test-suite/primitive/float/spec_conv.v
@@ -31,3 +31,16 @@ 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 89d76ab870..04c8ab035d 100644
--- a/test-suite/primitive/float/sqrt.v
+++ b/test-suite/primitive/float/sqrt.v
@@ -28,15 +28,22 @@ 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 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 af21d2c656..fc068cb585 100644
--- a/test-suite/primitive/float/sub.v
+++ b/test-suite/primitive/float/sub.v
@@ -7,6 +7,7 @@ Definition three := Eval compute in of_int63 3%int63.
 
 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).
 
@@ -15,37 +16,47 @@ Definition tiny := Eval compute in 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
index 53fad1a74c..82e00b8532 100644
--- a/test-suite/primitive/float/valid_binary_conv.v
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -31,3 +31,16 @@ 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).