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/PrintCminor.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'backend/PrintCminor.ml')

diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 6a745060..30884b18 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -223,7 +223,7 @@ let rec print_stmt p s =
   | Sswitch(e, cases, dfl) ->
       fprintf p "@[<v 2>switch (%a) {" print_expr e;
       List.iter
-        (fun (Coq_pair(n, x)) ->
+        (fun (n, x) ->
            fprintf p "@ case %ld: exit %d;\n" 
                      (camlint_of_coqint n) (camlint_of_nat x))
         cases;
@@ -262,7 +262,7 @@ let print_function p id f =
   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 ef ->
       () (* Todo? *)
-- 
cgit