mod change (-x)

[helm.git] / helm / software / matita / contribs / ng_assembly / emulator / memory / memory_func.ma

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
old mode 100755 (executable)
new mode 100644 (file)
index 9f75b54..d823d2e
--- 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
    ]
   ].