diff options
Diffstat (limited to 'flocq/Calc/Div.v')
| -rw-r--r-- | flocq/Calc/Div.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/flocq/Calc/Div.v b/flocq/Calc/Div.v index 48e3bb51..88d99a1f 100644 --- a/flocq/Calc/Div.v +++ b/flocq/Calc/Div.v @@ -19,8 +19,9 @@ COPYING file for more details. (** * Helper function and theorem for computing the rounded quotient of two floating-point numbers. *) -From Coq Require Import Lia. -Require Import Raux Defs Generic_fmt Float_prop Digits Bracket. +From Coq Require Import ZArith Reals Lia. + +Require Import Zaux Raux Defs Generic_fmt Float_prop Digits Bracket. Set Implicit Arguments. Set Strongly Strict Implicit. |