diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-14 20:25:58 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-14 20:25:58 +0100 |
| commit | fb87921df88bf99385514fabb21458482e058260 (patch) | |
| tree | 0d35f528864822a6e309f1bd00a6f5daf858ce4e | |
| parent | 4f4608206a72815f4c09952a16786435b0206ca0 (diff) | |
| download | compcert-kvx-fb87921df88bf99385514fabb21458482e058260.tar.gz compcert-kvx-fb87921df88bf99385514fabb21458482e058260.zip | |
stuff
| -rw-r--r-- | kvx/FPDivision.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index ebf9136d..fad99f76 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -50,6 +50,8 @@ Proof. all: set (invb_d := (Float.of_single (ExtFloat32.inv (Float32.of_intu b)))). all: set (b_d := (Float.of_longu (Int64.repr (Int.unsigned b)))). all: cbn. + - admit. + - admit. Admitted. Definition approx_div a b := @@ -155,7 +157,7 @@ Proof. 2: lia. { unfold div_approx_reals. - fold a' b' prod_r. + fold a' b' prod' prod_r. unfold Int64.mul. rewrite Int64.unsigned_repr by admit. rewrite Int64.unsigned_repr by admit. |