Change return type of primitive float comparison

Replace `option comparison` with `float_comparison` (:= `FEq | FLt |
FGt | FNotComparable`) as suggested by Guillaume Melquiond to avoid
boxing and an extra match when using primitive float comparison.

1 files changed, 6 insertions, 6 deletions

diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v
index 04c91cd56a..8aa9b4ca45 100644
--- a/test-suite/primitive/float/double_rounding.v
+++ b/test-suite/primitive/float/double_rounding.v
@@ -7,8 +7,8 @@ Definition small_cbn := Eval cbn in (one + 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 = Some Gt).
-Check (eq_refl : (check_cbn ?= big_cbn)%float = Some Eq).
+Check (eq_refl : (result_cbn ?= big_cbn)%float = FGt).
+Check (eq_refl : (check_cbn ?= big_cbn)%float = FEq).
 
 
 Definition big_cbv := Eval cbv in ldexp one (53)%Z.
@@ -16,8 +16,8 @@ Definition small_cbv := Eval cbv in (one + 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 = Some Gt).
-Check (eq_refl : (check_cbv ?= big_cbv)%float = Some Eq).
+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 ldexp one (53)%Z.
@@ -25,5 +25,5 @@ Definition small_vm := Eval vm_compute in (one + ldexp one (-52)%Z)%float.
 Definition result_vm := Eval vm_compute in (big_vm + small_vm)%float.
 Definition check_vm := Eval vm_compute in (big_vm + one)%float.
 
-Check (eq_refl : (result_vm ?= big_vm)%float = Some Gt).
-Check (eq_refl : (check_vm ?= big_vm)%float = Some Eq).
+Check (eq_refl : (result_vm ?= big_vm)%float = FGt).
+Check (eq_refl : (check_vm ?= big_vm)%float = FEq).