diff options
Diffstat (limited to 'flocq/Core/Defs.v')
| -rw-r--r-- | flocq/Core/Defs.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/flocq/Core/Defs.v b/flocq/Core/Defs.v index 27342df9..4a199e01 100644 --- a/flocq/Core/Defs.v +++ b/flocq/Core/Defs.v @@ -18,7 +18,10 @@ COPYING file for more details. *) (** * Basic definitions: float and rounding property *) -Require Import Raux. + +From Coq Require Import ZArith Reals. + +Require Import Raux Zaux. Section Def. |