freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
index 371dc403364fe150da433790b6649b26c9f8f9f0..71e6e65eed4b684ea58bc5a9f8cb42ba1fe0ca79 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/opcode_base_lemmas.ma
@@ -41,25 +41,25 @@ ndefinition mcu_type_destruct : mcu_type_destruct_aux.
  nelim m1;
  ##[ ##1: nelim m2; nnormalize; #H;
           ##[ ##1: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match HC05 with [ HC05 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##2: nelim m2; nnormalize; #H;
           ##[ ##2: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match HC08 with [ HC08 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##3: nelim m2; nnormalize; #H;
           ##[ ##3: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match HCS08 with [ HCS08 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
  ##| ##4: nelim m2; nnormalize; #H;
           ##[ ##4: napply (λx:P.x)
-          ##| ##*: napply (False_ind (λ_.?) ?);
+          ##| ##*: napply False_ind;
                    nchange with (match RS08 with [ RS08 ⇒ False | _ ⇒ True ]);
                    nrewrite > H; nnormalize; napply I
           ##]
@@ -71,7 +71,7 @@ nlemma symmetric_eqmcutype : symmetricT mcu_type bool eq_mcutype.
  nelim m1;
  nelim m2;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m2).
@@ -79,8 +79,8 @@ nlemma eqmcutype_to_eq : ∀m1,m2:mcu_type.(eq_mcutype m1 m2 = true) → (m1 = m
  ncases m1;
  ncases m2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (bool_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (bool_destruct … H)
  ##]
 nqed.
 
@@ -89,8 +89,8 @@ nlemma eq_to_eqmcutype : ∀m1,m2.m1 = m2 → eq_mcutype m1 m2 = true.
  ncases m1;
  ncases m2;
  nnormalize;
- ##[ ##1,6,11,16: #H; napply (refl_eq ??)
- ##| ##*: #H; napply (mcu_type_destruct ??? H)
+ ##[ ##1,6,11,16: #H; napply refl_eq
+ ##| ##*: #H; napply (mcu_type_destruct … H)
  ##]
 nqed.
 
@@ -99,7 +99,7 @@ nlemma instr_mode_destruct_MODE_DIRn : ∀n1,n2.MODE_DIRn n1 = MODE_DIRn n2 →
  nchange with (match MODE_DIRn n2 with [ MODE_DIRn a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 = MODE_DIRn_and_IMM1 n2 → n1 = n2.
@@ -107,7 +107,7 @@ nlemma instr_mode_destruct_MODE_DIRn_and_IMM1 : ∀n1,n2.MODE_DIRn_and_IMM1 n1 =
  nchange with (match MODE_DIRn_and_IMM1 n2 with [ MODE_DIRn_and_IMM1 a ⇒ n1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma instr_mode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1 = e2.
@@ -115,7 +115,7 @@ nlemma instr_mode_destruct_MODE_TNY : ∀e1,e2.MODE_TNY e1 = MODE_TNY e2 → e1
  nchange with (match MODE_TNY e2 with [ MODE_TNY a ⇒ e1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma instr_mode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1 = t2.
@@ -123,5 +123,5 @@ nlemma instr_mode_destruct_MODE_SRT : ∀t1,t2.MODE_SRT t1 = MODE_SRT t2 → t1
  nchange with (match MODE_SRT t2 with [ MODE_SRT a ⇒ t1 = a | _ ⇒ False ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.