From 056068abd228fefab4951a61700aa6d54fb88287 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 29 Jan 2013 09:10:29 +0000
Subject: Ported to Coq 8.4pl1.  Merge of branches/coq-8.4.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2101 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/PrintAsm.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'arm/PrintAsm.ml')

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 6415248..9d09fc1 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -719,7 +719,7 @@ let print_init oc = function
       fprintf oc "	.quad	%Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.bits_of_double n))
 	comment (camlfloat_of_coqfloat n)
   | Init_space n ->
-      let n = camlint_of_z n in
+      let n = Z.to_int32 n in
       if n > 0l then fprintf oc "	.space	%ld\n" n
   | Init_addrof(symb, ofs) ->
       fprintf oc "	.word	%a\n" print_symb_ofs (symb, ofs)
-- 
cgit v1.2.3