diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 21:20:44 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 21:20:44 +0100 |
| commit | de209fbba248e47f703f90c90817041cfdbf3d06 (patch) | |
| tree | 02586584395047d6374149629d7ca134785a99cf /kvx | |
| parent | 7b0c81a907ea5b772561b910acdf1efd615451b6 (diff) | |
| download | compcert-kvx-de209fbba248e47f703f90c90817041cfdbf3d06.tar.gz compcert-kvx-de209fbba248e47f703f90c90817041cfdbf3d06.zip | |
one admit less
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index b71c8990..37aa76ea 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -96,7 +96,10 @@ Proof. pose proof (BofZ_correct 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b') as C1. rewrite Rlt_bool_true in C1; cycle 1. { clear C1. cbn. - admit. + assert (1 <= (round radix2 (FLT_exp (-149) 24) ZnearestE (IZR b')) <= 4294967296)%R. + gappa. + apply Rabs_lt. + lra. } rewrite Zlt_bool_false in C1 by lia. destruct C1 as (C1E & C1F & _). |