summaryrefslogtreecommitdiff
path: root/arm/PrintAsm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r--arm/PrintAsm.ml2
1 files changed, 1 insertions, 1 deletions
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)