diff options
Diffstat (limited to 'theories/Floats/PrimFloat.v')
| -rw-r--r-- | theories/Floats/PrimFloat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Floats/PrimFloat.v b/theories/Floats/PrimFloat.v index ed7947aa63..4c818a7e52 100644 --- a/theories/Floats/PrimFloat.v +++ b/theories/Floats/PrimFloat.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Int63 FloatClass. +Require Import PrimInt63 FloatClass. (** * Definition of the interface for primitive floating-point arithmetic |