freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / test_errori.ma

diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma
index 155b6073fe79eb1019284f7f5ba2e0531ad0597f..4236c5c6341f7c0b93e878951e88b04880244284 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/test_errori.ma
+++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma
@@ -1,7 +1,6 @@
 
-include "utility/utility.ma".
+(*include "utility/utility.ma".
 
-(*
 nlemma fold_right_neList2_aux3 :
 \forall T. \forall h,h',t,t'.len_neList T (h§§t) = len_neList T (h'§§t') → len_neList T t = len_neList T t'.
  #T; #h; #h'; #t; #t';
@@ -22,9 +21,8 @@ nlemma fold_right_neList2_aux3 :
           nchange in H2:(%) with ((S (len_neList T (a§§l1))) = (S (len_neList T (a§§l))));
 *)
 
-include "freescale/byte8_lemmas.ma".
+(*include "freescale/byte8_lemmas.ma".
 
-(*
 nlemma associative_plusb8_aux
  : \forall e1,e2,e3,e4.
   match plus_ex_d_dc e2 e4 with
@@ -70,9 +68,8 @@ nlemma associative_plusb8
  (*...*)
 *)
 
-include "compiler/ast_type_lemmas.ma".
+(*include "compiler/ast_type_lemmas.ma".
 
-(*
 nlemma symmetric_eqasttype_aux1
  : ∀x1,x2,y2.eq_nat (len_neList ast_type («£x1»)) (len_neList ast_type (x2§§y2)) = false.
  #x1; #x2; #y2; ncases y2; nnormalize;