diff options
| author | Maxime Dénès <maxime.denes@inria.fr> | 2019-07-04 20:02:59 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-04 20:02:59 +0200 |
| commit | da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074 (patch) | |
| tree | 78320e4b422033d2b1a64937ccf00c6fe5ab748e | |
| parent | 8dc7fb147fb49294ccc4357b0c566b7e007c680f (diff) | |
| download | compcert-da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074.tar.gz compcert-da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074.zip | |
Avoid relying on `Export` bug (#301)
The previous code was unintentionally relying on a strange behavior of `Export` (see https://github.com/coq/coq/issues/10480) that will be removed.
| -rw-r--r-- | lib/Floats.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 9540303b..8b118c8d 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -24,6 +24,7 @@ Require Import Program. Require Archi. Close Scope R_scope. +Open Scope Z_scope. Definition float := binary64. (**r the type of IEE754 double-precision FP numbers *) Definition float32 := binary32. (**r the type of IEE754 single-precision FP numbers *) @@ -1218,7 +1219,7 @@ Proof. assert (C: m / 2^p = if zeq (n mod 2^p) 0 then 0 else 1). { unfold m. destruct (zeq (n mod 2^p) 0). rewrite e. apply Z.div_small. omega. - eapply Zdiv_unique with (n mod 2^p - 1). ring. omega. } + eapply Coqlib.Zdiv_unique with (n mod 2^p - 1). ring. omega. } assert (D: Z.testbit m p = if zeq (n mod 2^p) 0 then false else true). { destruct (zeq (n mod 2^p) 0). apply Z.testbit_false; auto. rewrite C; auto. |