From cdcb658c29409c8aef94ca3e22c14a90b396aea0 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 18 Oct 2011 09:40:59 +0000
Subject: Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to
 Caml chars

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/PrintAsm.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'powerpc')

diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 3b90ada..91dd686 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -920,7 +920,7 @@ let stub_function =
   | MacOS       -> Stubs_MacOS.stub_function
   | Linux|Diab  -> Stubs_EABI.stub_function
 
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
   match defn with
   | Internal code ->
       print_function oc name code
@@ -929,7 +929,7 @@ let print_fundef oc (Coq_pair(name, defn)) =
   | External _ ->
       ()
 
-let record_extfun (Coq_pair(name, defn)) =
+let record_extfun (name, defn) =
   match defn with
   | Internal _ -> ()
   | External (EF_external _) ->
@@ -967,7 +967,7 @@ let print_init_data oc name id =
   else
     List.iter (print_init oc) id
 
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
   match v.gvar_init with
   | [] -> ()
   | _  ->
-- 
cgit v1.2.3