1 files changed, 0 insertions, 3 deletions
diff --git a/arm/Asm.v b/arm/Asm.v
index 60dae47..6d5edf7 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -608,9 +608,6 @@ Definition preg_of (r: mreg) : preg :=
     We exploit the calling conventions from module [Conventions], except that
     we use ARM registers instead of locations. *)
 
-Definition chunk_of_type (ty: typ) :=
-  match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end.
-
 Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
   | extcall_arg_reg: forall r,
       extcall_arg rs m (R r) (rs (preg_of r))