diff options
Diffstat (limited to 'flocq/Prop/Sterbenz.v')
| -rw-r--r-- | flocq/Prop/Sterbenz.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/flocq/Prop/Sterbenz.v b/flocq/Prop/Sterbenz.v index 9594ac5d..8f516d0e 100644 --- a/flocq/Prop/Sterbenz.v +++ b/flocq/Prop/Sterbenz.v @@ -19,7 +19,9 @@ COPYING file for more details. (** * Sterbenz conditions for exact subtraction *) -Require Import Raux Defs Generic_fmt Operations. +From Coq Require Import ZArith Reals. + +Require Import Zaux Raux Defs Generic_fmt Operations. Section Fprop_Sterbenz. |