diff options
Diffstat (limited to 'test-suite/primitive/float')
| -rw-r--r-- | test-suite/primitive/float/double_rounding.v | 12 |
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). |