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 a4394d4f1947e88cdf5a493a62b33998f18f9c5c..371dc403364fe150da433790b6649b26c9f8f9f0 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
           ##]