diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-04-24 14:02:32 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-26 13:59:17 +0200 |
| commit | 08fd5faf30c18e17caa610076e67cf002a01d8b4 (patch) | |
| tree | f88a2e1b3de21ebb748850c1b8bf13f3d715979e /lib/Floats.v | |
| parent | 51c497b2e5a2b09788f2cf05f414634b037f52bf (diff) | |
| download | compcert-kvx-08fd5faf30c18e17caa610076e67cf002a01d8b4.tar.gz compcert-kvx-08fd5faf30c18e17caa610076e67cf002a01d8b4.zip | |
Move Z definitions out of Integers and into Zbits
The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size. These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.
This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.
Diffstat (limited to 'lib/Floats.v')
| -rw-r--r-- | lib/Floats.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index f93505fc..21d09a5e 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -16,8 +16,7 @@ (** Formalization of floating-point numbers, using the Flocq library. *) -Require Import Coqlib. -Require Import Integers. +Require Import Coqlib Zbits Integers. (*From Flocq*) Require Import Binary Bits Core. Require Import Fappli_IEEE_extra. @@ -1356,9 +1355,9 @@ Proof. rewrite Int64.testbit_repr by auto. f_equal. f_equal. unfold Int64.and. change (Int64.unsigned (Int64.repr 2047)) with 2047. change 2047 with (Z.ones 11). rewrite ! Z.land_ones by omega. - rewrite Int64.unsigned_repr. apply Int64.eqmod_mod_eq. + rewrite Int64.unsigned_repr. apply eqmod_mod_eq. apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega. - apply Int64.eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned. + apply eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned. exists (2^(64-11)); auto. exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto. assert (2^11 < Int64.max_unsigned) by (compute; auto). omega. |