diff options
Diffstat (limited to 'flocq/Prop/Round_odd.v')
| -rw-r--r-- | flocq/Prop/Round_odd.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/flocq/Prop/Round_odd.v b/flocq/Prop/Round_odd.v index a433c381..a7d98eb4 100644 --- a/flocq/Prop/Round_odd.v +++ b/flocq/Prop/Round_odd.v @@ -20,7 +20,8 @@ COPYING file for more details. (** * Rounding to odd and its properties, including the equivalence between rnd_NE and double rounding with rnd_odd and then rnd_NE *) -Require Import Reals Psatz. +From Coq Require Import ZArith Reals Psatz. + Require Import Core Operations. Definition Zrnd_odd x := match Req_EM_T x (IZR (Zfloor x)) with |