diff options
Diffstat (limited to 'lib/Floats.v')
| -rw-r--r-- | lib/Floats.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 6857236d..2e60d73e 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -23,7 +23,7 @@ Require Import Coqlib. Require Import Integers. -Parameter float: Set. +Parameter float: Type. Module Float. |