diff options
Diffstat (limited to 'flocq/Prop/Relative.v')
| -rw-r--r-- | flocq/Prop/Relative.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/flocq/Prop/Relative.v b/flocq/Prop/Relative.v index 6b8e8f77..a87e5666 100644 --- a/flocq/Prop/Relative.v +++ b/flocq/Prop/Relative.v @@ -18,8 +18,10 @@ COPYING file for more details. *) (** * Relative error of the roundings *) + +From Coq Require Import ZArith Reals Psatz. + Require Import Core. -Require Import Psatz. (* for lra *) Section Fprop_relative. |