From 76555ffd2403b3ebf1ea353063c16763e6493722 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 6 May 2013 11:32:22 +0000
Subject: Refactoring: move definition of chunk_of_type to AST.v.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2238 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/Asm.v | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'arm')

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))
-- 
cgit v1.2.3