1 files changed, 0 insertions, 3 deletions
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 2757061..09dead3 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -720,9 +720,6 @@ Definition preg_of (r: mreg) : preg :=
     We exploit the calling conventions from module [Conventions], except that
     we use machine 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))