X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fread_write%2FFreescale_load_write.ma;h=38c9053e3e949600b7d02322040aa5e39e8bd7ff;hb=826883e023c178930ca3dd69567eac23f15ef9c4;hp=f14b38b19530cd6af530b9f38f89775e054faa6e;hpb=2c38e6a237e6a0e263abccf8d8ef3e7a31272443;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma
index f14b38b19..38c9053e3 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/read_write/Freescale_load_write.ma
@@ -195,7 +195,7 @@ ndefinition aux_inc_indX_16 ≝
    (λs_tmp.Some ? s_tmp)).
 
 ndefinition Freescale_multi_mode_load_auxb ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH  ⇒ None ?
 (* restituisce A *)
@@ -276,7 +276,7 @@ ndefinition Freescale_multi_mode_load_auxb ≝
    ].
 
 ndefinition Freescale_multi_mode_load_auxw ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.match i with
 (* NO: non ci sono indicazioni *)
    [ MODE_INH  ⇒ None ?
 (* NO: solo lettura/scrittura byte *)
@@ -417,7 +417,7 @@ ndefinition Freescale_multi_mode_load_auxw ≝
 (* **************************************** *)
 
 ndefinition Freescale_multi_mode_write_auxb ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λflag:aux_mod_type.λ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 *)
@@ -507,7 +507,7 @@ ndefinition Freescale_multi_mode_write_auxb ≝
   ].
 
 ndefinition Freescale_multi_mode_write_auxw ≝
-λm,t.λs:any_status m t.λpco,cur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
+λm,t.λs:any_status m t.λcur_pc:word16.λi:Freescale_instr_mode.λwritew:word16.match i with
 (* NO: non ci sono indicazioni *)
   [ MODE_INH        ⇒ None ?
 (* NO: solo lettura/scrittura byte *)