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
---
 cfrontend/PrintCsyntax.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'cfrontend/PrintCsyntax.ml')

diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 63587869..f0e9ee54 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -312,7 +312,7 @@ let name_function_parameters fun_name params =
   | _ ->
       let rec add_params first = function
       | [] -> ()
-      | Coq_pair(id, ty) :: rem ->
+      | (id, ty) :: rem ->
           if not first then Buffer.add_string b ", ";
           Buffer.add_string b (name_cdecl (extern_atom id) ty);
           add_params false rem in
@@ -328,13 +328,13 @@ let print_function p id f =
                         f.fn_return);
   fprintf p "@[<v 2>{@ ";
   List.iter
-    (fun (Coq_pair(id, ty)) ->
+    (fun (id, ty) ->
       fprintf p "%s;@ " (name_cdecl (extern_atom id) ty))
     f.fn_vars;
   print_stmt p f.fn_body;
   fprintf p "@;<0 -2>}@]@ @ "
 
-let print_fundef p (Coq_pair(id, fd)) =
+let print_fundef p (id, fd) =
   match fd with
   | External(_, args, res) ->
       fprintf p "extern %s;@ @ "
@@ -374,7 +374,7 @@ let print_init p = function
 
 let re_string_literal = Str.regexp "__stringlit_[0-9]+"
 
-let print_globvar p (Coq_pair(id, v)) =
+let print_globvar p (id, v) =
   let name1 = extern_atom id in
   let name2 = if v.gvar_readonly then "const " ^ name1 else name1 in
   let name3 = if v.gvar_volatile then "volatile " ^ name2 else name2 in
@@ -469,16 +469,16 @@ and collect_cases = function
 
 let collect_function f =
   collect_type f.fn_return;
-  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_params;
-  List.iter (fun (Coq_pair(id, ty)) -> collect_type ty) f.fn_vars;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_params;
+  List.iter (fun (id, ty) -> collect_type ty) f.fn_vars;
   collect_stmt f.fn_body
 
-let collect_fundef (Coq_pair(id, fd)) =
+let collect_fundef (id, fd) =
   match fd with
   | External(_, args, res) -> collect_type_list args; collect_type res
   | Internal f -> collect_function f
 
-let collect_globvar (Coq_pair(id, v)) =
+let collect_globvar (id, v) =
   collect_type v.gvar_info
 
 let collect_program p =
-- 
cgit