diff options
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 f91dca6..897a2ee 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) -> |