diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 21:57:25 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-16 21:57:25 +0100 |
| commit | 18ec7b4072aef0160e96915d13218381f4420c4c (patch) | |
| tree | 4a3cce90c4968cd3ef7fee9e288d2e835a48f54b /kvx | |
| parent | f3510994276cfc73fb2f8441f652c97259753d81 (diff) | |
| download | compcert-kvx-18ec7b4072aef0160e96915d13218381f4420c4c.tar.gz compcert-kvx-18ec7b4072aef0160e96915d13218381f4420c4c.zip | |
one admit less
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/FPDivision.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/kvx/FPDivision.v b/kvx/FPDivision.v index 2b99f392..fed327b7 100644 --- a/kvx/FPDivision.v +++ b/kvx/FPDivision.v @@ -122,7 +122,7 @@ Proof. (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) b')) as C2. rewrite Rlt_bool_true in C2; cycle 1. { clear C2. rewrite C1E. - apply (Rabs_relax (bpow radix2 24) (bpow radix2 128)). + apply (Rabs_relax (bpow radix2 10)). { cbn; lra. } unfold F2R. cbn. unfold F2R. cbn. gappa. @@ -149,7 +149,13 @@ Proof. fold invb_d in C3. rewrite Rlt_bool_true in C3; cycle 1. { clear C3. - admit. + rewrite C2E. + rewrite C1E. + rewrite C0E. + apply (Rabs_relax (bpow radix2 10)). + { cbn; lra. } + cbn. + gappa. } change (is_finite 24 128 (BofZ 24 128 (@eq_refl Datatypes.comparison Lt) (@eq_refl Datatypes.comparison Lt) 1)) with true in C2F. destruct (C3 C2F) as (C3E & C3F & _). |