diff options
Diffstat (limited to 'flocq/Core/FLX.v')
| -rw-r--r-- | flocq/Core/FLX.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/flocq/Core/FLX.v b/flocq/Core/FLX.v index 78bffba5..c1abf639 100644 --- a/flocq/Core/FLX.v +++ b/flocq/Core/FLX.v @@ -18,9 +18,10 @@ COPYING file for more details. *) (** * Floating-point format without underflow *) -Require Import Raux Defs Round_pred Generic_fmt Float_prop. -Require Import FIX Ulp Round_NE. -Require Import Psatz. + +From Coq Require Import ZArith Reals Psatz. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop FIX Ulp Round_NE. Section RND_FLX. |