diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-09 16:01:44 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-03-09 16:01:44 +0100 |
| commit | d5f60d876d51380cb8119084c29aa062ca417c45 (patch) | |
| tree | 7931a2416b230afe5814fbd60894630e51129b52 | |
| parent | 25e82e849de35eaef24412b468d3a36c72f4fcb6 (diff) | |
| download | compcert-kvx-master.tar.gz compcert-kvx-master.zip | |
| -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) |