diff options
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r-- | arm/PrintAsm.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 60d0fa41..0cee7865 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -637,6 +637,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 |