1 files changed, 4 insertions, 1 deletions
diff --git a/kvx/ExtFloats.v b/kvx/ExtFloats.v
index b08503a5..332d3e3d 100644
--- a/kvx/ExtFloats.v
+++ b/kvx/ExtFloats.v
@@ -13,6 +13,8 @@
 (*                                                             *)
 (* *************************************************************)
 
+From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
+                          Binary Round_odd.
 Require Import Floats Integers ZArith.
 
 Module ExtFloat.
@@ -30,6 +32,8 @@ Definition max (x : float) (y : float) : float :=
   | Some Eq | Some Gt => x
   | Some Lt | None => y
   end.
+
+Definition one := Float.of_int (Int.repr (1%Z)).
 End ExtFloat.
 
 Module ExtFloat32.
@@ -50,5 +54,4 @@ Definition max (x : float32) (y : float32) : float32 :=
 Definition one := Float32.of_int (Int.repr (1%Z)).
 Definition inv (x : float32) : float32 :=
   Float32.div one x.
-
 End ExtFloat32.