diff options
| -rw-r--r-- | kvx/FPDivision64.v | 2 |
1 files changed, 1 insertions, 1 deletions
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) |