A) New version.

[helm.git] / helm / software / matita / library / freescale / load_write.ma

diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/library/freescale/load_write.ma
index 9ed17612937cc471557f52548be5ecd28b27b49b..16df9aae4a1874b3168337a0e353656dc960b7ee 100644 (file)
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -24,9 +24,6 @@
 (*                    data ultima modifica 15/11/2007                     *)
 (* ********************************************************************** *)
 
-set "baseuri" "cic:/matita/freescale/load_write/".
-
-(*include "/media/VIRTUOSO/freescale/model.ma".*)
 include "freescale/model.ma".
 
 (* errori possibili nel fetch *)
@@ -350,8 +347,8 @@ definition writebit_to ≝
 definition writew_to ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λaddr:word16.λcur_pc:word16.λfetched:nat.λwritew:word16.
  opt_map ?? (memory_filter_write m t s addr (w16h writew))
-  (λtmps.opt_map ?? (memory_filter_write m t s (succ_w16 addr) (w16l writew))
-    (λtmps'.Some ? (pair ?? tmps' (filtered_plus_w16 m t s cur_pc fetched)))).
+  (λtmps1.opt_map ?? (memory_filter_write m t tmps1 (succ_w16 addr) (w16l writew))
+    (λtmps2.Some ? (pair ?? tmps2 (filtered_plus_w16 m t tmps2 cur_pc fetched)))).
 
 (* ausiliari per definire i tipi e la lettura/scrittura *)
 
@@ -371,7 +368,7 @@ definition aux_write_typing ≝
 λm:mcu_type.λt:memory_impl.λbyteflag:bool.
  any_status m t → word16 → word16 → nat →
  match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
- option (Prod (any_status m t) word16).
+ option (ProdT (any_status m t) word16).
 
 (* per non dover ramificare i vari load in byte/word *)
 definition aux_write ≝
@@ -744,7 +741,7 @@ definition multi_mode_write ≝
 λbyteflag:bool.λm:mcu_type.λt:memory_impl.match byteflag
  return λbyteflag:bool.any_status m t → word16 → instr_mode →
   match byteflag with [ true ⇒ byte8 | false ⇒ word16 ] →
-  option (Prod (any_status m t) word16) with
+  option (ProdT (any_status m t) word16) with
  (* scrittura di un byte *)
  [ true ⇒ λs:any_status m t.λcur_pc:word16.λi:instr_mode.λwriteb:byte8.match i with
 (* NO: non ci sono indicazioni *)