aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/PrintCsyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/PrintCsyntax.ml')
-rw-r--r--cfrontend/PrintCsyntax.ml3
1 files changed, 3 insertions, 0 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 03dc5837..97a00b09 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -268,6 +268,9 @@ let rec expr p (prec, e) =
| Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
fprintf p "__builtin_debug@[<hov 1>(%d,%S%a)@]"
(P.to_int kind) (extern_atom txt) exprlist (false,args)
+ | Ebuiltin(EF_builtin(name, _), _, args, _) ->
+ fprintf p "%s@[<hov 1>(%a)@]"
+ (camlstring_of_coqstring name) exprlist (true, args)
| Ebuiltin(_, _, args, _) ->
fprintf p "<unknown builtin>@[<hov 1>(%a)@]" exprlist (true, args)
| Eparen(a1, tycast, ty) ->