From 4297fcb821c3188449b64184af73e41491a6118f Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 23 Jul 2012 15:01:54 +0000
Subject: - Revised non-overflow constraints on memory injections so that  
 injections compose (Values, Memdata, Memory) - Memory chunks: Mfloat64 now
 has alignment 8; introduced Mfloat64al32   that works like old Mfloat64 (i.e.
 has alignment 4); simplified   handling of memcpy builtin accordingly.

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

(limited to 'arm/Op.v')

diff --git a/arm/Op.v b/arm/Op.v
index fa05288a..cfe8b834 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -342,17 +342,6 @@ Definition type_of_addressing (addr: addressing) : list typ :=
   | Ainstack _ => nil
   end.
 
-Definition type_of_chunk (c: memory_chunk) : typ :=
-  match c with
-  | Mint8signed => Tint
-  | Mint8unsigned => Tint
-  | Mint16signed => Tint
-  | Mint16unsigned => Tint
-  | Mint32 => Tint
-  | Mfloat32 => Tfloat
-  | Mfloat64 => Tfloat
-  end.
-
 (** Weak type soundness results for [eval_operation]:
   the result values, when defined, are always of the type predicted
   by [type_of_operation]. *)
-- 
cgit