diff options
| -rw-r--r-- | caml/PrintPPC.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index b9eb728..830de0d 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -326,9 +326,7 @@ let print_function oc (Coq_pair(name, code)) = coqlist_iter (print_instruction oc (labels_of_code code)) code let print_var oc (Coq_pair(name, size)) = - fprintf oc " .globl %a\n" print_symb name; - fprintf oc "%a:\n" print_symb name; - fprintf oc " .space %ld\n" (camlint_of_z size) + fprintf oc " .comm %a, %ld\n" print_symb name (camlint_of_z size) let print_program oc p = coqlist_iter (print_var oc) p.prog_vars; |