X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftranslation.ma;h=0996948942bad7c8c8cd7b4809456eaa72acc96b;hb=cad56a7b9eadce5aef71c5b14192181a847dde27;hp=94d254bf2fe709a1fddf082bc63200ba8e154c3c;hpb=03ebff6c48be2253ad32b3b57f4e1d2b02acda86;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
index 94d254bf2..099694894 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -15,8 +15,8 @@
 (* ********************************************************************** *)
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
+(*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
+(*   Ultima modifica: 05/08/2009                                          *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -24,7 +24,7 @@ include "freescale/table_HC05.ma".
 include "freescale/table_HC08.ma".
 include "freescale/table_HCS08.ma".
 include "freescale/table_RS08.ma".
-include "freescale/option.ma".
+include "common/option.ma".
 
 (* ***************************** *)
 (* TRADUZIONE ESADECIMALE → INFO *)
@@ -51,7 +51,7 @@ nlet rec full_info_of_word16_aux (m:mcu_type) (borw:byte8_or_word16)
  match param with
   [ nil ⇒ None ?
   | cons hd tl ⇒
-   match thd4T ???? hd with
+   match thd4T … hd with
     [ Byte b ⇒ match borw with
      [ Byte borw' ⇒ match eq_b8 borw' b with
       [ true ⇒ Some ? hd
@@ -76,13 +76,11 @@ full_info_of_word16_aux m borw (opcode_table m).
 ninductive t_byte8 (m:mcu_type) : Type ≝
  TByte : byte8 → t_byte8 m.
 
-nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
- #m; #b1; #b2; #H;
- nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
- nrewrite < H;
- nnormalize;
- napply (refl_eq ??).
-nqed.
+ndefinition eq_tbyte8 ≝
+λm.λtb1,tb2:t_byte8 m.
+ match tb1 with
+  [ TByte b1 ⇒ match tb2 with
+   [ TByte b2 ⇒ eq_b8 b1 b2 ]].
 
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
 ninductive MA_check : instr_mode → Type ≝
@@ -177,8 +175,8 @@ nlet rec bytes_of_pseudo_instr_mode_param_aux (m:mcu_type) (o:any_opcode m) (i:i
                                              (param:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on param ≝
  match param with
  [ nil ⇒ None ? | cons hd tl ⇒
-  match (eq_anyop m o (fst4T ???? hd)) ⊗ (eq_instrmode i (snd4T ???? hd)) with
-   [ true ⇒ match thd4T ???? hd with 
+  match (eq_anyop m o (fst4T … hd)) ⊗ (eq_im i (snd4T … hd)) with
+   [ true ⇒ match thd4T … hd with 
     [ Byte isab ⇒ 
      Some ? ([ (TByte m isab) ]@(args_picker m i p))
     | Word isaw ⇒