freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
index 2ae4388886a849b425cd2ed041862d22f8c24d94..bcb09a2f892f4d0fabc138f99ef8bd7ca80f8457 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
@@ -40,12 +40,12 @@ ndefinition bool_destruct : bool_destruct_aux.
  nelim b2;
  nnormalize;
  #H;
- ##[ ##2: napply (False_ind (λx.?) ?);
+ ##[ ##2: napply False_ind;
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite > H;
           nnormalize;
           napply I
- ##| ##3: napply (False_ind (λx.?) ?);
+ ##| ##3: napply False_ind;
           nchange with (match true with [ true ⇒ False | false ⇒ True]);
           nrewrite < H;
           nnormalize;