diff options
Diffstat (limited to 'ia32/PrintAsm.ml')
| -rw-r--r-- | ia32/PrintAsm.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 08bd2f5..da08de8 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -714,6 +714,10 @@ let print_instruction oc = function (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> print_annot_val oc (extern_atom txt) args res + | EF_inline_asm txt -> + fprintf oc "%s begin inline assembly\n" comment; + fprintf oc " %s\n" (extern_atom txt); + fprintf oc "%s end inline assembly\n" comment | _ -> assert false end |