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
---
 arm/PrintAsm.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'arm')

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 50b585e..a616cc2 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -201,7 +201,7 @@ let call_helper oc fn dst arg1 arg2 =
   let moves =
     Parmov.parmove2 (=) (fun _ -> IR14) [arg1; arg2] [IR0; IR1] in
   List.iter
-    (fun (Coq_pair(s, d)) ->
+    (fun (s, d) ->
       fprintf oc "	mov	%a, %a\n" ireg d ireg s)
     moves;
   (* Call the helper function *)
@@ -689,7 +689,7 @@ let print_function oc name fn =
   fprintf oc "	.type	%a, %%function\n" print_symb name;
   fprintf oc "	.size	%a, . - %a\n" print_symb name print_symb name
 
-let print_fundef oc (Coq_pair(name, defn)) =
+let print_fundef oc (name, defn) =
   match defn with
   | Internal code ->
       print_function oc name code
@@ -729,7 +729,7 @@ let rec log2 n =
   assert (n > 0);
   if n = 1 then 0 else 1 + log2 (n lsr 1)
 
-let print_var oc (Coq_pair(name, v)) =
+let print_var oc (name, v) =
   match v.gvar_init with
   | [] -> ()
   | _  ->
-- 
cgit v1.2.3