diff options
Diffstat (limited to 'flocq/Core/Round_pred.v')
| -rw-r--r-- | flocq/Core/Round_pred.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/flocq/Core/Round_pred.v b/flocq/Core/Round_pred.v index b7b6778f..c811aec8 100644 --- a/flocq/Core/Round_pred.v +++ b/flocq/Core/Round_pred.v @@ -18,6 +18,9 @@ COPYING file for more details. *) (** * Roundings: properties and/or functions *) + +From Coq Require Import Reals. + Require Import Raux Defs. Section RND_prop. |