1 files changed, 3 insertions, 3 deletions
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 39de282b..d890c820 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -123,7 +123,7 @@ let rec name_cdecl id ty =
           if not first then Buffer.add_string b ", ";
           Buffer.add_string b (name_cdecl "" t1);
           add_args false tl in
-      add_args true args;
+      if not cconv.cc_unproto then add_args true args;
       Buffer.add_char b ')';
       name_cdecl (Buffer.contents b) res
   | Tstruct(name, a) ->
@@ -299,9 +299,9 @@ and extended_asm p txt res args clob =
   begin match clob with
   | [] -> ()
   | c1 :: cl ->
-      fprintf p "@ : @[<hov 0>%S" (extern_atom c1);
+      fprintf p "@ : @[<hov 0>%S" (camlstring_of_coqstring c1);
       List.iter
-        (fun c -> fprintf p ",@ %S" (extern_atom c))
+        (fun c -> fprintf p ",@ %S" (camlstring_of_coqstring c))
         cl;
       fprintf p "@]"
   end;