From 2b5f5cb0bb6d8dbf302ab6d84c27eda30252912d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Mar 2016 10:23:18 +0100 Subject: Add support for EF_runtime externals Also: in Events, use Senv.equiv to state invariance wrt changes of global envs. --- cfrontend/PrintCsyntax.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'cfrontend/PrintCsyntax.ml') diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index bb6576aa..d5853e38 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -264,6 +264,8 @@ let rec expr p (prec, e) = (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_external(id, sg), _, args, _) -> fprintf p "%s@[(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) + | Ebuiltin(EF_runtime(id, sg), _, args, _) -> + fprintf p "%s@[(%a)@]" (camlstring_of_coqstring id) exprlist (true, args) | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) -> extended_asm p txt None args clob | Ebuiltin(EF_debug(kind,txt,_),_,args,_) -> @@ -427,7 +429,7 @@ let print_function p id f = let print_fundef p id fd = match fd with - | External(EF_external(_,_), args, res, cconv) -> + | External((EF_external _ | EF_runtime _), args, res, cconv) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res, cconv))) | External(_, _, _, _) -> -- cgit