From 30dd68d627f68cca0c2addd006d853379ad720cf Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 28 Jan 2015 16:51:28 +0100
Subject: Changed the print_globaldef function of the powerpc backend to look
 like the functions used in the arm and ia32 backend.

---
 powerpc/PrintAsm.ml | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index f058cde5..0c4356ec 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -750,15 +750,6 @@ let print_function oc name fn =
     jumptables := []
   end
 
-(* Generation of whole programs *)
-
-let print_fundef oc name defn =
-  match defn with
-  | Internal code ->
-      print_function oc name code
-  | External _ ->
-      ()
-
 let print_init oc = function
   | Init_int8 n ->
       fprintf oc "	.byte	%ld\n" (camlint_of_coqint n)
@@ -831,7 +822,8 @@ let print_var oc name v =
 
 let print_globdef oc (name, gdef) =
   match gdef with
-  | Gfun f -> print_fundef oc name f
+  | Gfun (Internal code) -> print_function oc name code
+  | Gfun (External ef) ->   ()
   | Gvar v -> print_var oc name v
 
   end
-- 
cgit