X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fread_write%2Fload_write.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fread_write%2Fload_write.ma;h=3c24d528c12d8ff0801b15b4338a520b77166365;hb=826883e023c178930ca3dd69567eac23f15ef9c4;hp=73db58f81666818c284eb98cd1f9d49b469fbf47;hpb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma
index 73db58f81..3c24d528c 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/load_write.ma
@@ -29,7 +29,7 @@ include "emulator/read_write/IP2022_load_write.ma".
 
 ndefinition multi_mode_loadb ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m →
+    return λm.Πt.any_status m t → word16 → aux_im_type m →
               option (Prod3T (any_status m t) byte8 word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_load_auxb HC05
@@ -41,7 +41,7 @@ ndefinition multi_mode_loadb ≝
 
 ndefinition multi_mode_loadw ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m →
+    return λm.Πt.any_status m t → word16 → aux_im_type m →
                  option (Prod3T (any_status m t) word16 word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_load_auxw HC05
@@ -51,15 +51,13 @@ ndefinition multi_mode_loadw ≝
     | IP2022 ⇒ IP2022_multi_mode_load_auxw
   ].
 
-(* tutte le modalita' di lettura: false=loadb true=loadw *)
-
 (* **************************************** *)
 (* raccordo di tutte le possibili scritture *)
 (* **************************************** *)
 
 ndefinition multi_mode_writeb ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → word16 → aux_mod_type → aux_im_type m → byte8 →
+    return λm.Πt.any_status m t → word16 → aux_mod_type → aux_im_type m → byte8 →
               option (ProdT (any_status m t) word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_write_auxb HC05
@@ -71,7 +69,7 @@ ndefinition multi_mode_writeb ≝
 
 ndefinition multi_mode_writew ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m → word16 →
+    return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
               option (ProdT (any_status m t) word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05