fixed deps

[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 16df9aae4a1874b3168337a0e353656dc960b7ee..a5fae5375e8f52197421f35ffddded2e7e5e6fdf 100644 (file)
--- a/helm/software/matita/library/freescale/load_write.ma
+++ b/helm/software/matita/library/freescale/load_write.ma
@@ -260,10 +260,12 @@ definition filtered_inc_w16 ≝
 λm:mcu_type.λt:memory_impl.λs:any_status m t.λw:word16.
  get_pc_reg m t (set_pc_reg m t s (succ_w16 w)).
 
-let rec filtered_plus_w16 (m:mcu_type) (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
+definition filtered_plus_w16 := \lambda m:mcu_type.
+let rec filtered_plus_w16  (t:memory_impl) (s:any_status m t) (w:word16) (n:nat) on n ≝
  match n with
   [ O ⇒ w
-  | S n' ⇒ filtered_plus_w16 m t s (filtered_inc_w16 m t s w) n' ].
+  | S n' ⇒ filtered_plus_w16 t s (filtered_inc_w16 m t s w) n' ]
+in filtered_plus_w16.
 
 (* 
    errore1: non esiste traduzione ILL_OP
@@ -368,7 +370,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 (ProdT (any_status m t) word16).
+ option (Prod (any_status m t) word16).
 
 (* per non dover ramificare i vari load in byte/word *)
 definition aux_write ≝
@@ -741,7 +743,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 (ProdT (any_status m t) word16) with
+  option (Prod (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 *)