From 2bf69a09c20c52685ce3c1933577b9aaa5e38e51 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 9 Nov 2017 14:27:23 +0100
Subject: Removed no longer used function. Bug 22525

---
 arm/TargetPrinter.ml | 26 +-------------------------
 1 file changed, 1 insertion(+), 25 deletions(-)

(limited to 'arm/TargetPrinter.ml')

diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index 1493f9fc..0cd3c908 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -51,10 +51,7 @@ struct
 
   let symbol = elf_symbol
 
-  let symbol_offset oc (symb, ofs) =
-    symbol oc symb;
-    let ofs = camlint_of_coqint ofs in
-    if ofs <> 0l then fprintf oc " + %ld" ofs
+  let symbol_offset = elf_symbol_offset
 
   let int_reg_name = function
     | IR0 -> "r0" | IR1 -> "r1" | IR2 -> "r2" | IR3 -> "r3"
@@ -839,27 +836,6 @@ struct
 
   (* Data *)
 
-  let print_init oc = function
-    | Init_int8 n ->
-      fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
-    | Init_int16 n ->
-      fprintf oc "	.short	%ld\n" (camlint_of_coqint n)
-    | Init_int32 n ->
-      fprintf oc "	.word	%ld\n" (camlint_of_coqint n)
-    | Init_int64 n ->
-      fprintf oc "	.quad	%Ld\n" (camlint64_of_coqint n)
-    | Init_float32 n ->
-      fprintf oc "	.word	0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float32.to_bits n))
-        comment (camlfloat_of_coqfloat32 n)
-    | Init_float64 n ->
-      fprintf oc "	.quad	%Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.to_bits n))
-        comment (camlfloat_of_coqfloat n)
-    | Init_space 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" symbol_offset (symb, ofs)
-
   let print_prologue oc =
     fprintf oc "	.syntax	unified\n";
     fprintf oc "	.arch	%s\n"
-- 
cgit