1) \ldots here and there

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma
index 34b5c43af8aaa2a5bc8e2e326c1a9dd8012e0dee..faef75e9a16a275ae1823b853e9f64dc3c12a610 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode.ma
@@ -31,7 +31,7 @@ nlet rec get_byte_count (m:mcu_type) (b:byte8) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
-  | cons hd tl ⇒ match thd4T ???? hd with
+  | cons hd tl ⇒ match thd4T … hd with
    [ Byte b' ⇒ match eq_b8 b b' with
     [ true ⇒ get_byte_count m b (S c) tl
     | false ⇒ get_byte_count m b c tl
@@ -45,7 +45,7 @@ nlet rec get_word_count (m:mcu_type) (b:byte8) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
-  | cons hd tl ⇒ match thd4T ???? hd with
+  | cons hd tl ⇒ match thd4T … hd with
    [ Byte _ ⇒ get_word_count m b c tl
    | Word w ⇒ match eq_w16 〈〈x9,xE〉:b〉 w with
     [ true ⇒ get_word_count m b (S c) tl
@@ -59,7 +59,7 @@ nlet rec get_pseudo_count (m:mcu_type) (o:opcode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
-  | cons hd tl ⇒ match fst4T ???? hd with
+  | cons hd tl ⇒ match fst4T … hd with
    [ anyOP o' ⇒ match eq_op o o' with
     [ true ⇒ get_pseudo_count m o (S c) tl
     | false ⇒ get_pseudo_count m o c tl
@@ -72,7 +72,7 @@ nlet rec get_mode_count (m:mcu_type) (i:instr_mode) (c:nat)
  (l:list (Prod4T (any_opcode m) instr_mode byte8_or_word16 byte8)) on l ≝
  match l with
   [ nil ⇒ c
-  | cons hd tl ⇒ match eq_instrmode (snd4T ???? hd) i with
+  | cons hd tl ⇒ match eq_instrmode (snd4T … hd) i with
    [ true ⇒ get_mode_count m i (S c) tl
    | false ⇒ get_mode_count m i c tl
    ]
@@ -114,8 +114,8 @@ nlet rec get_OpIm_count (m:mcu_type) (o:any_opcode m) (i:instr_mode) (c:nat)
  match l with
   [ nil ⇒ c
   | cons hd tl ⇒
-   match (eq_anyop m o (fst4T ???? hd)) ⊗
-         (eq_instrmode i (snd4T ???? hd)) with
+   match (eq_anyop m o (fst4T … hd)) ⊗
+         (eq_instrmode i (snd4T … hd)) with
     [ true ⇒ get_OpIm_count m o i (S c) tl
     | false ⇒ get_OpIm_count m o i c tl
     ]