Don't print external declarations for builtins.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1818 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 4 insertions, 2 deletions

diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 83a0747..77f22f7 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;