1) \ldots here and there

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / translation.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
index 94d254bf2fe709a1fddf082bc63200ba8e154c3c..9b327ac1fe1961f76c39671cd9f695bc623b4859 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/translation.ma
@@ -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_instrmode i (snd4T … hd)) with
+   [ true ⇒ match thd4T … hd with 
     [ Byte isab ⇒ 
      Some ? ([ (TByte m isab) ]@(args_picker m i p))
     | Word isaw ⇒