X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Ftranslation%2Ftranslation.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Ftranslation%2Ftranslation.ma;h=c507eac1796371e673b44c0ec151ebc41755116a;hb=6ee4fa0ba5f4b6601b62afd482d4f30bd2de2f91;hp=4cd470862e77c701c76ac0c2e3daaae250e37812;hpb=8899a3f240f62633f4df58b2ee358fa285a82d1d;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma index 4cd470862..c507eac17 100755 --- a/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma +++ b/helm/software/matita/contribs/ng_assembly/emulator/translation/translation.ma @@ -67,7 +67,7 @@ nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:aux_op_type m) (i: [ Byte isab ⇒ Some ? ([ (TByte m isab) ]@(args_picker m i p)) | Word isaw ⇒ - Some ? ([ (TByte m (w16h isaw)) ; (TByte m (w16l isaw)) ]@(args_picker m i p)) + Some ? ([ (TByte m (cnH ? isaw)) ; (TByte m (cnL ? isaw)) ]@(args_picker m i p)) ] | false ⇒ bytes_of_pseudo_instr_mode_param_aux m o i p tl ]].