X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_bits.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_bits.ma;h=c49be931a4594557c071b882db33619a67513a94;hb=bf0cc84dcef9ae3d2145e79754bb39feb3985574;hp=93dcfa53f7f0fa5ff44e14b8eff618044ee71e6f;hpb=c2b39b7ef14ab610cb2056fb6b75492c7068288e;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
index 93dcfa53f..c49be931a 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_bits.ma
@@ -215,13 +215,9 @@ let newbit7 ≝ match getn_array8T o7 memory_type bit_types with
 
 (* carica a paratire da addr, scartando source (pescando da old_mem) se si supera 0xFFFF... *)
 nlet rec mb_load_from_source_at (old_mem:Array16T (Array16T (Array16T (Array16T (Array8T bool)))))
-                               (source:list byte8) (addr:word16) on source ≝
-match source with
- (* fine di source: carica da old_mem *)
- [ nil ⇒ old_mem
- | cons hd tl ⇒ match lt_w16 addr 〈〈xF,xF〉:〈xF,xF〉〉 with
-  (* non supera 0xFFFF, ricorsione *)
-  [ true ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
-  (* supera 0xFFFF, niente ricorsione *)
-  | false ⇒ mt_update ? old_mem addr (bits_of_byte8 hd)
-  ]].
+                                (src:list byte8) (addr:word16) on src ≝
+ match src with
+  (* fine di source: carica da old_mem *)
+  [ nil ⇒ old_mem
+  | cons hd tl ⇒ mb_load_from_source_at (mt_update ? old_mem addr (bits_of_byte8 hd)) tl (plus_w16_d_d addr 〈〈x0,x0〉:〈x0,x1〉〉)
+  ].