From e46fa563d09371c74994957e260b7db14df9a7db Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 17 Aug 2015 11:24:47 +0200
Subject: Update clightgen w.r.t. EF_inline_asm (type of the clobber list).

---
 exportclight/ExportClight.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'exportclight/ExportClight.ml')

diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 397d04b1..9f8d596c 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -135,6 +135,11 @@ let coqsingle p n =
 let coqN p n =
   fprintf p "%ld%%N" (N.to_int32 n)
 
+(* Coq strings *)
+
+let coqstring p s =
+  fprintf p "\"%s\"" (camlstring_of_coqstring s)
+
 (* Raw attributes *)
 
 let attribute p a =
@@ -262,7 +267,7 @@ let external_function p = function
       fprintf p "@[<hov 2>(EF_inline_asm %ld%%positive@ %a@ %a)@]"
               (P.to_int32 text)
               signatur sg
-              (print_list ident) clob
+              (print_list coqstring) clob
 
 (* Expressions *)
 
-- 
cgit