diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 09:35:23 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2022-01-24 09:35:23 +0100 |
| commit | fa79debdca4121f2435750b8090e83b541887979 (patch) | |
| tree | 2da74e7b8aab6ae0b22c3c313db27e4a1c5ae100 /kvx/FPDivision64.v | |
| parent | a7db868181d74403449ce436028f0658f284088e (diff) | |
| download | compcert-kvx-fa79debdca4121f2435750b8090e83b541887979.tar.gz compcert-kvx-fa79debdca4121f2435750b8090e83b541887979.zip | |
progress
Diffstat (limited to 'kvx/FPDivision64.v')
| -rw-r--r-- | kvx/FPDivision64.v | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/kvx/FPDivision64.v b/kvx/FPDivision64.v index 0dfa9882..8d40e88e 100644 --- a/kvx/FPDivision64.v +++ b/kvx/FPDivision64.v @@ -1145,7 +1145,7 @@ Proof. lia. } destruct (BofZ_exact 53 1024 re re (Int64.signed a) SILLY) as (C1R & C1F & C1S). - fold a' in C1R. + fold a' in C1R, C1F, C1S. pose proof (Bmult_correct 53 1024 re re Float.binop_nan mode_NE (BofZ 53 1024 re re a') f) as C2. rewrite Rlt_bool_true in C2 ; cycle 1. { clear C2. @@ -1160,7 +1160,14 @@ Proof. unfold smalla_thresh in *. gappa. } - cbn. + rewrite C0F in C2. + rewrite C1R in C2. + rewrite C1F in C2. + rewrite C1S in C2. + cbn in C2. + destruct C2 as (C2R & C2F & _). + rewrite C2R. + admit. Admitted. Definition step2_div_long' a b := |