diff options
Diffstat (limited to 'exportclight')
-rw-r--r-- | exportclight/ExportClight.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index b124586a..d86e137a 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -381,7 +381,7 @@ and lblstmts p = function (print_option coqZ) lbl stmt s lblstmts ls let print_function p (id, f) = - fprintf p "Definition f_%s := {|@ " (extern_atom id); + fprintf p "Definition f_%s := {|@ " (sanitize (extern_atom id)); fprintf p " fn_return := %a;@ " typ f.fn_return; fprintf p " fn_callconv := %a;@ " callconv f.fn_callconv; fprintf p " fn_params := %a;@ " (print_list (print_pair ident typ)) f.fn_params; @@ -402,7 +402,7 @@ let init_data p = function | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs let print_variable p (id, v) = - fprintf p "Definition v_%s := {|@ " (extern_atom id); + fprintf p "Definition v_%s := {|@ " (sanitize (extern_atom id)); fprintf p " gvar_info := %a;@ " typ v.gvar_info; fprintf p " gvar_init := %a;@ " (print_list init_data) v.gvar_init; fprintf p " gvar_readonly := %B;@ " v.gvar_readonly; @@ -417,12 +417,12 @@ let print_globdef p (id, gd) = let print_ident_globdef p = function | (id, Gfun(Ctypes.Internal f)) -> - fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id) + fprintf p "(%a, Gfun(Internal f_%s))" ident id (sanitize (extern_atom id)) | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) -> fprintf p "@[<hov 2>(%a,@ @[<hov 2>Gfun(External %a@ %a@ %a@ %a))@]@]" ident id external_function ef typlist targs typ tres callconv cc | (id, Gvar v) -> - fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id) + fprintf p "(%a, Gvar v_%s)" ident id (sanitize (extern_atom id)) (* Composite definitions *) |