From ef40c6d36f1c3125f3aa78ea4eaa61dcc7bcae67 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Thu, 19 Nov 2009 13:32:09 +0000
Subject: Revised lib/Integers.v to make it parametric w.r.t. word size.
 Introduced Int.iwordsize and used it in place of "Int.repr 32" or "Int.repr
 (Z_of_nat wordsize)".

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

(limited to 'powerpc/Asm.v')

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 1582b41..60c3d34 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -302,9 +302,7 @@ lbl:    .long   0x43300000, 0x00000000
         lwz     r12, lo16(lbl)(r12)
         mtctr   r12
         bctr    r12
-        .const_data
 lbl:    .long   table[0], table[1], ...
-        .text
 >>
   Note that [reg] contains 4 times the index of the desired table entry.
 *)
-- 
cgit v1.2.3