summaryrefslogtreecommitdiff
path: root/arm/PrintAsm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r--arm/PrintAsm.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 9d09fc1..d90d7b6 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -719,8 +719,8 @@ 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 = Z.to_int32 n in
- if n > 0l then fprintf oc " .space %ld\n" n
+ if Z.gt n Z.zero then
+ fprintf oc " .space %s\n" (Z.to_string n)
| Init_addrof(symb, ofs) ->
fprintf oc " .word %a\n" print_symb_ofs (symb, ofs)