X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Ftranslation.ma;h=661737793505a9660d138755d3ea7311128c3f9f;hb=38fccc2b774e493a94eedef76342b56079c0e694;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..661737793 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
@@ -81,7 +81,7 @@ nlemma tbyte8_destruct : ∀m,b1,b2.TByte m b1 = TByte m b2 → b1 = b2.
  nchange with (match TByte m b2 with [ TByte a ⇒ b1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 (* introduzione di un tipo dipendente (dalla modalita') per gli argomenti *)
@@ -177,8 +177,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 ⇒