diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-25 11:47:59 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-09-25 11:47:59 +0200 |
| commit | 2dd133f9178ae285d3939f29479b4acd9dad394d (patch) | |
| tree | a89023c15848438f84b47663633f34960b9bcfbc /flocq/IEEE754/Binary.v | |
| parent | c34d25e011402aedad62b3fe9b7b04989df4522e (diff) | |
| download | compcert-kvx-2dd133f9178ae285d3939f29479b4acd9dad394d.tar.gz compcert-kvx-2dd133f9178ae285d3939f29479b4acd9dad394d.zip | |
Update the vendored Flocq library to version 3.4.2
For compatibility with the upcoming Coq 8.14.
Diffstat (limited to 'flocq/IEEE754/Binary.v')
| -rw-r--r-- | flocq/IEEE754/Binary.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/flocq/IEEE754/Binary.v b/flocq/IEEE754/Binary.v index 35d15cb3..4516f0a0 100644 --- a/flocq/IEEE754/Binary.v +++ b/flocq/IEEE754/Binary.v @@ -2472,9 +2472,9 @@ case f. now revert Hover; unfold B2R, F2R; simpl; rewrite Rmult_assoc, bpow_plus. Qed. -(** This hypothesis is needed to implement Bfrexp +(** This hypothesis is needed to implement [Bfrexp] (otherwise, we have emin > - prec - and Bfrexp cannot fit the mantissa in interval [0.5, 1)) *) + and [Bfrexp] cannot fit the mantissa in interval #[0.5, 1)#) *) Hypothesis Hemax : (3 <= emax)%Z. Definition Ffrexp_core_binary s m e := |