diff options
Diffstat (limited to 'flocq/Prop/Div_sqrt_error.v')
| -rw-r--r-- | flocq/Prop/Div_sqrt_error.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/flocq/Prop/Div_sqrt_error.v b/flocq/Prop/Div_sqrt_error.v index 9aa9c508..49c46b7e 100644 --- a/flocq/Prop/Div_sqrt_error.v +++ b/flocq/Prop/Div_sqrt_error.v @@ -19,7 +19,8 @@ COPYING file for more details. (** * Remainder of the division and square root are in the FLX format *) -Require Import Psatz. +From Coq Require Import ZArith Reals Psatz. + Require Import Core Operations Relative Sterbenz Mult_error. Section Fprop_divsqrt_error. |