aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 94f13aa1..6ecdb14e 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -847,7 +847,7 @@ let convertAsm loc env txt outputs inputs clobber =
let (txt', output', inputs') =
ExtendedAsm.transf_asm loc env txt outputs inputs clobber in
let clobber' =
- List.map intern_string clobber in
+ List.map (fun s -> coqstring_of_camlstring (String.uppercase s)) clobber in
let ty_res =
match output' with None -> TVoid [] | Some e -> e.etyp in
(* Build the Ebuiltin expression *)