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
---
 backend/LTL.v       | 10 ----------
 backend/Locations.v |  2 +-
 backend/Mach.v      |  3 ---
 3 files changed, 1 insertion(+), 14 deletions(-)

(limited to 'backend')

diff --git a/backend/LTL.v b/backend/LTL.v
index de10845..27fee8a 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -197,16 +197,6 @@ Definition parent_locset (stack: list stackframe) : locset :=
   | Stackframe f sp ls bb :: stack' => ls
   end.
 
-(* REVISE
-(** [getslot sl ofs ty rs] looks up the value of location [S sl ofs ty] in [rs],
-  and normalizes it to the type [ty] of this location. *)
-
-Definition getslot (sl: slot) (ofs: Z) (ty: typ) (rs: locset) : val :=
-  Val.load_result
-    (match ty with Tint => Mint32 | Tfloat => Mfloat64 | Tlong => Mint64 end)
-    (rs (S sl ofs ty)).
-*)
-
 Inductive step: state -> trace -> state -> Prop :=
   | exec_start_block: forall s f sp pc rs m bb,
       (fn_code f)!pc = Some bb ->
diff --git a/backend/Locations.v b/backend/Locations.v
index 2f2dae8..f7fb607 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -273,7 +273,7 @@ End Loc.
 
 (** The [Locmap] module defines mappings from locations to values,
   used as evaluation environments for the semantics of the [LTL] 
-  and [LTLin] intermediate languages.  *)
+  and [Linear] intermediate languages.  *)
 
 Set Implicit Arguments.
 
diff --git a/backend/Mach.v b/backend/Mach.v
index 5030de1..ec48195 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -123,9 +123,6 @@ value of the return address that the Asm code generated later will
 store in the reserved location.
 *)
 
-Definition chunk_of_type (ty: typ) :=
-  match ty with Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 end.
-
 Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) :=
   Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)).
 
-- 
cgit v1.2.3