diff options
Diffstat (limited to 'flocq/Calc/Round.v')
| -rw-r--r-- | flocq/Calc/Round.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/flocq/Calc/Round.v b/flocq/Calc/Round.v index 704a1ab2..40da2f08 100644 --- a/flocq/Calc/Round.v +++ b/flocq/Calc/Round.v @@ -19,7 +19,8 @@ COPYING file for more details. (** * Helper function for computing the rounded value of a real number. *) -From Coq Require Import Lia. +From Coq Require Import ZArith Reals Lia. + Require Import Core Digits Float_prop Bracket. Section Fcalc_round. |