(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / read_write / load_write.ma

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 683a0f7afb323986df345e178d4385f4a6c4b497..73db58f81666818c284eb98cd1f9d49b469fbf47 100755 (executable)
--- 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 → aux_im_type m →
+    return λm.Πt.any_status m t → word16 → 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 → aux_im_type m →
+    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m →
                  option (Prod3T (any_status m t) word16 word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_load_auxw HC05
@@ -59,7 +59,7 @@ ndefinition multi_mode_loadw ≝
 
 ndefinition multi_mode_writeb ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → aux_im_type m → byte8 →
+    return λm.Πt.any_status m t → word16 → 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 +71,7 @@ ndefinition multi_mode_writeb ≝
 
 ndefinition multi_mode_writew ≝
 λm.match m
-    return λm.Πt.any_status m t → word16 → aux_im_type m → word16 →
+    return λm.Πt.any_status m t → word16 → word16 → aux_im_type m → word16 →
               option (ProdT (any_status m t) word16)
    with
     [ HC05 ⇒ Freescale_multi_mode_write_auxw HC05