X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Femulator%2Fmemory%2Fmemory_func.ma;h=d823d2e8d4f70e035a29bbab276951fdbbaf66c9;hb=eb4144a401147a44a9620169eb6dafeb8f5a2c17;hp=9f75b5497f06afae7a4771fd9ed0c91ef0c2cc05;hpb=a79bf6edc13daaea8135ca71fdc92e02e229f030;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma
index 9f75b5497..d823d2e8d 100755
--- a/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma
+++ b/helm/software/matita/contribs/ng_assembly/emulator/memory/memory_func.ma
@@ -32,7 +32,7 @@ include "common/list.ma".
 (* (mf_check_update_ranged chk inf sup mode) = setta tipo memoria *)
 ndefinition mf_check_update_ranged ≝
 λf:word32 → memory_type.λaddr:word32.λrange:word16.λv.
- λx.match inrange_w32 x addr (plus_w32_d_d addr 〈〈〈x0,x0〉:〈x0,x0〉〉.range〉) with
+ λx.match inrange_w32 x addr (plus_w32_d_d addr (ext_word32 range)) with
   [ true ⇒ v
   | false ⇒ f x ].
 
@@ -74,6 +74,6 @@ nlet rec mf_load_from_source_at (old_mem:word32 → byte8) (src:list byte8) (add
    (* la locazione corrisponde al punto corrente di source *)
    [ true ⇒ hd
    (* la locazione e' piu' avanti? ricorsione *)
-   | false ⇒ (mf_load_from_source_at old_mem tl (plus_w32_d_d addr 〈〈〈x0,x0〉:〈x0,x0〉〉.〈〈x0,x0〉:〈x0,x1〉〉〉)) x
+   | false ⇒ (mf_load_from_source_at old_mem tl (succ_w32 addr)) x
    ]
   ].