1 files changed, 0 insertions, 39 deletions
diff --git a/mppa_k1c/ExtFloats.v b/mppa_k1c/ExtFloats.v
deleted file mode 100644
index d9b9d3a6..00000000
--- a/mppa_k1c/ExtFloats.v
+++ /dev/null
@@ -1,39 +0,0 @@
-Require Import Floats Integers ZArith.
-
-Module ExtFloat.
-(** TODO check with the actual K1c;
-    this is what happens on x86 and may be inappropriate. *)
-
-Definition min (x : float) (y : float) : float :=
-  match Float.compare x y with
-  | Some Eq | Some Lt => x
-  | Some Gt | None => y
-  end.
-
-Definition max (x : float) (y : float) : float :=
-  match Float.compare x y with
-  | Some Eq | Some Gt => x
-  | Some Lt | None => y
-  end.
-End ExtFloat.
-
-Module ExtFloat32.
-(** TODO check with the actual K1c *)
-
-Definition min (x : float32) (y : float32) : float32 :=
-  match Float32.compare x y with
-  | Some Eq | Some Lt => x
-  | Some Gt | None => y
-  end.
-
-Definition max (x : float32) (y : float32) : float32 :=
-  match Float32.compare x y with
-  | Some Eq | Some Gt => x
-  | Some Lt | None => y
-  end.
-
-Definition one := Float32.of_int (Int.repr (1%Z)).
-Definition inv (x : float32) : float32 :=
-  Float32.div one x.
-
-End ExtFloat32.