From 7998ccfd709b97f1a2306df4570365d58a5bb4b5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 12 Jan 2014 10:48:56 +0000 Subject: - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4. - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'common/AST.v') diff --git a/common/AST.v b/common/AST.v index 5eee2917..6f35be01 100644 --- a/common/AST.v +++ b/common/AST.v @@ -133,8 +133,7 @@ Inductive memory_chunk : Type := | Mint32 (**r 32-bit integer, or pointer *) | Mint64 (**r 64-bit integer *) | Mfloat32 (**r 32-bit single-precision float *) - | Mfloat64 (**r 64-bit double-precision float *) - | Mfloat64al32. (**r 64-bit double-precision float, 4-aligned *) + | Mfloat64. (**r 64-bit double-precision float *) Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}. Proof. decide equality. Defined. @@ -152,7 +151,6 @@ Definition type_of_chunk (c: memory_chunk) : typ := | Mint64 => Tlong | Mfloat32 => Tsingle | Mfloat64 => Tfloat - | Mfloat64al32 => Tfloat end. Definition type_of_chunk_use (c: memory_chunk) : typ := @@ -165,7 +163,6 @@ Definition type_of_chunk_use (c: memory_chunk) : typ := | Mint64 => Tlong | Mfloat32 => Tfloat | Mfloat64 => Tfloat - | Mfloat64al32 => Tfloat end. (** The chunk that is appropriate to store and reload a value of @@ -174,7 +171,7 @@ Definition type_of_chunk_use (c: memory_chunk) : typ := Definition chunk_of_type (ty: typ) := match ty with | Tint => Mint32 - | Tfloat => Mfloat64al32 + | Tfloat => Mfloat64 | Tlong => Mint64 | Tsingle => Mfloat32 end. -- cgit