X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fstatus%2Fstatus.ma;h=927da3d25f3f9fd5c6daeb0e1f78ad016a1fb42f;hb=b31c093c364e76cc6c4657008f3f259955311911;hp=0456997fc9f7c2a6fd6ff9647b0742a5f45027d9;hpb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
index 0456997fc..927da3d25 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/status/status.ma
@@ -34,7 +34,7 @@ include "emulator/opcodes/pseudo.ma".
 (* descrittore del click = stato di avanzamento dell'esecuzione *)
 (* 1) None = istruzione eseguita, attesa del fetch *)
 (* 2) Some cur_clk,pseudo,mode,clks,cur_pc = fetch eseguito *)
-ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_op_type m) (aux_im_type m) byte8 word16.
+ndefinition aux_clk_type ≝ λm:mcu_type.Prod5T byte8 (aux_pseudo_type m) (aux_im_type m) byte8 word16.
 
 (* tipo processore dipendente dalla mcu, varia solo la ALU *)
 nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
@@ -93,7 +93,7 @@ nlet rec forall_memory_ranged
                  (forall_memory_ranged t chk1 chk2 mem1 mem2 tl)
   ].
 
-ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_op m) (eq_im m) eq_b8 eq_w16).
+ndefinition eq_clk ≝ λm.eq_option … (eq_quintuple … eq_b8 (eq_pseudo m) (eq_im m) eq_b8 eq_w16).
 
 (* generalizzazione del confronto fra stati *)
 ndefinition eq_anystatus ≝