diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2020-09-08 18:29:00 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-04-25 16:38:45 +0200 |
commit | 9aacc59135071a979623ab177819cdbe9ce27056 (patch) | |
tree | 1d2069eba895833fdb3a7647c3cc37cea32a0de6 /flocq/Core/Generic_fmt.v | |
parent | fb1f4545dfe861ff4d02816e295021a7e3061687 (diff) | |
download | compcert-9aacc59135071a979623ab177819cdbe9ce27056.tar.gz compcert-9aacc59135071a979623ab177819cdbe9ce27056.zip |
Upgrade to Flocq 4.0.
Diffstat (limited to 'flocq/Core/Generic_fmt.v')
-rw-r--r-- | flocq/Core/Generic_fmt.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/flocq/Core/Generic_fmt.v b/flocq/Core/Generic_fmt.v index af1bf3c1..b3b71b19 100644 --- a/flocq/Core/Generic_fmt.v +++ b/flocq/Core/Generic_fmt.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * What is a real number belonging to a format, and many properties. *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Float_prop. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Float_prop. Section Generic. @@ -427,7 +428,7 @@ rewrite Gx. replace (Ztrunc (scaled_mantissa x)) with Z0. apply F2R_0. cut (Z.abs (Ztrunc (scaled_mantissa x)) < 1)%Z. -clear ; zify ; lia. +clear ; lia. apply lt_IZR. rewrite abs_IZR. now rewrite <- scaled_mantissa_generic. @@ -1804,7 +1805,7 @@ Theorem Znearest_imp : Proof. intros x n Hd. cut (Z.abs (Znearest x - n) < 1)%Z. -clear ; zify ; lia. +clear ; lia. apply lt_IZR. rewrite abs_IZR, minus_IZR. replace (IZR (Znearest x) - IZR n)%R with (- (x - IZR (Znearest x)) + (x - IZR n))%R by ring. |