1 files changed, 0 insertions, 28 deletions
diff --git a/common/Values.v b/common/Values.v
index 059a72d9..127d1085 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -767,34 +767,6 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
   end.
 
 
-Definition extfz stop start v :=
-  if (Z.leb start stop)
-       && (Z.geb start Z.zero)
-       && (Z.ltb stop Int.zwordsize)
-  then
-    let stop' := Z.add stop Z.one in
-    match v with
-    | Vint w =>
-      Vint (Int.shru (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
-    | _ => Vundef
-    end
-  else Vundef.
-
-
-Definition extfs stop start v :=
-  if (Z.leb start stop)
-       && (Z.geb start Z.zero)
-       && (Z.ltb stop Int.zwordsize)
-  then
-    let stop' := Z.add stop Z.one in
-    match v with
-    | Vint w =>
-      Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
-    | _ => Vundef
-    end
-  else Vundef.
-
-
 (** Comparisons *)
 
 Section COMPARISONS.