From d5f60d876d51380cb8119084c29aa062ca417c45 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Mar 2022 16:01:44 +0100 Subject: enlarge range --- kvx/FPDivision64.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 298831a0..6b192d12 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -999,7 +999,7 @@ Qed. Definition step2_real_div_long a b := Val.mulf (Val.maketotal (Val.floatoflong a)) (approx_inv_longu b). -Definition smalla_thresh := 34184372088832%Z. +Definition smalla_thresh := 34200000000000%Z. Lemma step2_real_div_long_smalla_correct : forall (a b : int64) -- cgit