diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/PrintClight.ml | 6 | ||||
-rw-r--r-- | cfrontend/PrintCsyntax.ml | 6 |
2 files changed, 8 insertions, 4 deletions
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml index 83a07473..77f22f74 100644 --- a/cfrontend/PrintClight.ml +++ b/cfrontend/PrintClight.ml @@ -245,9 +245,11 @@ let print_function p id f = let print_fundef p (id, fd) = match fd with - | External(_, args, res) -> + | External(EF_external(_,_), args, res) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res))) + | External(_, _, _) -> + () | Internal f -> print_function p id f @@ -326,7 +328,7 @@ let print_struct_or_union p (name, fld) = fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); print_fields rem in print_fields fld; - fprintf p "@;<0 -2>};@]@ " + fprintf p "@;<0 -2>};@]@ @ " let print_program p prog = struct_unions := StructUnionSet.empty; diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index d4e728e8..804b0180 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -345,9 +345,11 @@ let print_function p id f = let print_fundef p (id, fd) = match fd with - | External(_, args, res) -> + | External(EF_external(_,_), args, res) -> fprintf p "extern %s;@ @ " (name_cdecl (extern_atom id) (Tfunction(args, res))) + | External(_, _, _) -> + () | Internal f -> print_function p id f @@ -505,7 +507,7 @@ let print_struct_or_union p (name, fld) = fprintf p "@ %s;" (name_cdecl (extern_atom id) ty); print_fields rem in print_fields fld; - fprintf p "@;<0 -2>};@]@ " + fprintf p "@;<0 -2>};@]@ @ " let print_program p prog = struct_unions := StructUnionSet.empty; |