diff options
| author | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-07 23:48:23 +0100 |
|---|---|---|
| committer | David Monniaux <David.Monniaux@univ-grenoble-alpes.fr> | 2021-12-07 23:48:23 +0100 |
| commit | 3ee28038f0596aaa89b72ffb6e905610c259b8b2 (patch) | |
| tree | 62ea1463361e89f71510adc61c925a6639f61f91 /lib | |
| parent | 0825b433dd2ebd947d5d4566ce8a3dfd8a98db88 (diff) | |
| parent | fbead38d40df6904dc0e446f673747b008c40022 (diff) | |
| download | compcert-kvx-3ee28038f0596aaa89b72ffb6e905610c259b8b2.tar.gz compcert-kvx-3ee28038f0596aaa89b72ffb6e905610c259b8b2.zip | |
Merge branch 'kvx_fp_division' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into kvx_fp_division
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/IEEE754_extra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 83cacb2b..56b90727 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1014,7 +1014,7 @@ Proof. rewrite plus_IZR. lra. Qed. - + Theorem ZofB_ne_correct: forall f, ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. |