From bb9d14a3f95fc0e3c8cad10d8ea8e2b2738da7fc Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 11 Jan 2009 11:57:02 +0000
Subject: - Added alignment constraints to memory loads and stores. - In Cminor
 and below, removed pointer validity check in semantics of   comparisons, so
 that evaluation of expressions is independent of   memory state. - In Cminor
 and below, removed "alloc" instruction. - Cleaned up commented-away parts.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 backend/Lineartyping.v | 2 --
 1 file changed, 2 deletions(-)

(limited to 'backend/Lineartyping.v')

diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 9ef6e317..33b570b9 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -85,8 +85,6 @@ Inductive wt_instr : instruction -> Prop :=
       tailcall_possible sig ->
       match ros with inl r => r = IT1 | _ => True end ->
       wt_instr (Ltailcall sig ros)
-  | wt_Lalloc:
-      wt_instr Lalloc
   | wt_Llabel:
       forall lbl,
       wt_instr (Llabel lbl)
-- 
cgit