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
---
 backend/CMparser.mly | 21 ++++++++++-----------
 1 file changed, 10 insertions(+), 11 deletions(-)

(limited to 'backend/CMparser.mly')

diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 0b48c0f..3df3f54 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -141,7 +141,7 @@ let mkswitch expr (cases, dfl) =
   let rec mktable = function
   | [] -> []
   | (key, exit) :: rem ->
-      Coq_pair(coqint_of_camlint key, exitnum exit) :: mktable rem in
+      (coqint_of_camlint key, exitnum exit) :: mktable rem in
   prepend_seq !convert_accu (Sswitch(c, mktable cases, exitnum dfl))
 
 (***
@@ -166,7 +166,7 @@ let mkmatch_aux expr cases =
     | [] -> assert false
     | [key, action] -> []
     | (key, action) :: rem ->
-        Coq_pair(coqint_of_camlint key, nat_of_camlint n)
+        (coqint_of_camlint key, nat_of_camlint n)
         :: mktable (Int32.succ n) rem in
   let sw =
     Sswitch(expr, mktable 0l cases, nat_of_camlint (Int32.pred ncases)) in
@@ -324,8 +324,8 @@ global_declarations:
 
 global_declaration:
     VAR STRINGLIT LBRACKET INTLIT RBRACKET
-      { Coq_pair($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
-                      gvar_readonly = false; gvar_volatile = false}) }
+      { ($2, {gvar_info = (); gvar_init = [Init_space(z_of_camlint $4)];
+              gvar_readonly = false; gvar_volatile = false}) }
 ;
 
 proc_list:
@@ -345,14 +345,13 @@ proc:
       { let tmp = !temporaries in
         temporaries := [];
         temp_counter := 0;
-        Coq_pair($1,
-        Internal { fn_sig = $6;
-                   fn_params = List.rev $3;
-                   fn_vars = List.rev (tmp @ $9);
-                   fn_stackspace = $8;
-                   fn_body = $10 }) }
+        ($1, Internal { fn_sig = $6;
+                        fn_params = List.rev $3;
+                        fn_vars = List.rev (tmp @ $9);
+                        fn_stackspace = $8;
+                        fn_body = $10 }) }
   | EXTERN STRINGLIT COLON signature 
-      { Coq_pair($2, External(EF_external($2, $4))) }
+      { ($2, External(EF_external($2, $4))) }
 ;
 
 signature:
-- 
cgit v1.2.3