diff options
Diffstat (limited to 'backend/Asmexpandaux.ml')
| -rw-r--r-- | backend/Asmexpandaux.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index f5c76925..0530abe4 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -96,7 +96,7 @@ let translate_annot sp preg_to_dwarf annot = | a::_ -> aux a) let builtin_nop = - let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in + let signature ={sig_args = []; sig_res = Tvoid; sig_cc = cc_default} in let name = coqstring_of_camlstring "__builtin_nop" in Pbuiltin(EF_builtin(name,signature),[],BR_none) |