diff options
Diffstat (limited to 'flocq/Core/FTZ.v')
| -rw-r--r-- | flocq/Core/FTZ.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/flocq/Core/FTZ.v b/flocq/Core/FTZ.v index d6bae6ea..e2c7ebad 100644 --- a/flocq/Core/FTZ.v +++ b/flocq/Core/FTZ.v @@ -19,9 +19,9 @@ COPYING file for more details. (** * Floating-point format with abrupt underflow *) -From Coq Require Import Lia. -Require Import Raux Defs Round_pred Generic_fmt. -Require Import Float_prop Ulp FLX. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Round_pred Generic_fmt Float_prop Ulp FLX. Section RND_FTZ. |