diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
| commit | cdcb658c29409c8aef94ca3e22c14a90b396aea0 (patch) | |
| tree | 8981d0a2312604c6b8ab8a8acb108f39f1cd1377 /backend/PrintCminor.ml | |
| parent | f535ac931c2b7dc65fefa83e47bb8c79ca90e92d (diff) | |
| download | compcert-kvx-cdcb658c29409c8aef94ca3e22c14a90b396aea0.tar.gz compcert-kvx-cdcb658c29409c8aef94ca3e22c14a90b396aea0.zip | |
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
Diffstat (limited to 'backend/PrintCminor.ml')
| -rw-r--r-- | backend/PrintCminor.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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? *) |