diff options
Diffstat (limited to 'lib/IEEE754_extra.v')
| -rw-r--r-- | lib/IEEE754_extra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index b0d1944e..fbcd527e 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -18,7 +18,7 @@ (** Additional operations and proofs about IEEE-754 binary floating-point numbers, on top of the Flocq library. *) -From Flocq Require Import Core Digits Operations Round Bracket Sterbenz +From kvx.Flocq Require Import Core Digits Operations Round Bracket Sterbenz Binary Round_odd. Require Import Psatz. Require Import Bool. |