diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Floats.v | 2 | ||||
| -rw-r--r-- | lib/IEEE754_extra.v (renamed from lib/Fappli_IEEE_extra.v) | 0 |
2 files changed, 1 insertions, 1 deletions
diff --git a/lib/Floats.v b/lib/Floats.v index 21d09a5e..9540303b 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -19,7 +19,7 @@ Require Import Coqlib Zbits Integers. (*From Flocq*) Require Import Binary Bits Core. -Require Import Fappli_IEEE_extra. +Require Import IEEE754_extra. Require Import Program. Require Archi. diff --git a/lib/Fappli_IEEE_extra.v b/lib/IEEE754_extra.v index c23149be..c23149be 100644 --- a/lib/Fappli_IEEE_extra.v +++ b/lib/IEEE754_extra.v |