]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma
mod change (-x)
[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / read_write / Freescale_load_write.ma
old mode 100755 (executable)
new mode 100644 (file)
index be04ff2..38c9053
@@ -20,8 +20,8 @@
 (*                                                                        *)
 (* ********************************************************************** *)
 
-include "emulator/read_write/load_write_base.ma".
 include "emulator/status/status_getter.ma".
+include "emulator/read_write/load_write_base.ma".
 
 (* lettura da [curpc]: IMM1 *)
 ndefinition mode_IMM1_load ≝
@@ -417,7 +417,7 @@ ndefinition Freescale_multi_mode_load_auxw ≝
 (* **************************************** *)
 
 ndefinition Freescale_multi_mode_write_auxb ≝
-λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwriteb:byte8.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λflag:aux_mod_type.λi:Freescale_instr_mode.λwriteb:byte8.match i with
 (* NO: non ci sono indicazioni *)
   [ MODE_INH        ⇒ None ?
 (* scrive A *)