diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:18:07 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-05-17 08:18:07 +0000 |
| commit | f692ee29c1ea8748120ca1a4cbb4cd7f1eb2531e (patch) | |
| tree | 9cc9ccd22b5010ef9d16e9a2a1017741d0ff6e13 /cfrontend/PrintCsyntax.ml | |
| parent | 807d49a50b126bd1013de110128cfe2ac22f02dc (diff) | |
| download | compcert-kvx-f692ee29c1ea8748120ca1a4cbb4cd7f1eb2531e.tar.gz compcert-kvx-f692ee29c1ea8748120ca1a4cbb4cd7f1eb2531e.zip | |
Preliminary support for debugging info (-g).
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2253 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
| -rw-r--r-- | cfrontend/PrintCsyntax.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index f91dca66..897a2ee5 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -242,11 +242,11 @@ let rec expr p (prec, e) = (camlint_of_coqint sz) (camlint_of_coqint al) exprlist (true, args) | Ebuiltin(EF_annot(txt, _), _, args, _) -> - fprintf p "__builtin_annot@[<hov 1>(%S,@ %a)@]" - (extern_atom txt) exprlist (true, args) + fprintf p "__builtin_annot@[<hov 1>(%S%a)@]" + (extern_atom txt) exprlist (false, args) | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> - fprintf p "__builtin_annot_val@[<hov 1>(%S,@ %a)@]" - (extern_atom txt) exprlist (true, args) + fprintf p "__builtin_annot_val@[<hov 1>(%S%a)@]" + (extern_atom txt) exprlist (false, args) | Ebuiltin(_, _, args, _) -> fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args) | Eparen(a1, ty) -> |