From da929bc61ccd67d2be2b1e5d3cd9f3cb60f56074 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 4 Jul 2019 20:02:59 +0200 Subject: 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. --- lib/Floats.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'lib/Floats.v') 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. -- cgit