diff options
Diffstat (limited to 'flocq/Core/Round_NE.v')
| -rw-r--r-- | flocq/Core/Round_NE.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/flocq/Core/Round_NE.v b/flocq/Core/Round_NE.v index b7387a62..6a6fb0fb 100644 --- a/flocq/Core/Round_NE.v +++ b/flocq/Core/Round_NE.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * Rounding to nearest, ties to even: existence, unicity... *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp. Notation ZnearestE := (Znearest (fun x => negb (Z.even x))). |