X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Ftests%2Fbad_tests%2Fauto.log;fp=matita%2Ftests%2Fbad_tests%2Fauto.log;h=0cac60da334790dbad4051c260f1dde434e405a7;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/matita/tests/bad_tests/auto.log b/matita/tests/bad_tests/auto.log
new file mode 100644
index 000000000..0cac60da3
--- /dev/null
+++ b/matita/tests/bad_tests/auto.log
@@ -0,0 +1,100 @@
+Info:  execution of auto.ma started:
+Debug: Executing: ``set "baseuri" "cic:/matita/tests/auto/"''
+Debug: Executing: ``include cic:/matita/legacy/coq''
+Debug: Executing: ``Theorem a: @[\forall ((x): (@[nat])).(\forall ((y) ...''
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Datatypes/nat.ind
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/eq.ind
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/minus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult.con
+Error: Bad name: a
+Debug: Executing: ``intro.''
+Debug: Executing: ``auto.''
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/trans_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/z.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal3.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/B.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/f.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/add_sub_square_identity.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_Sm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/semantics/conservation_0_0.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/technical_lemma.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/ARITH/Chinese/Nat_complements/technical_lemma.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/plus_minus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_minus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_plus_distr_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_plus_distr2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_n.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/minus_minus_lem1.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Cachan/SMC/mu/Splus_nm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_Sm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_Sn_m.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_Snm_nSm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/bases/S_plus_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/mult_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute_2_in_4.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_comm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc_reverse.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_permute2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_eq_decompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/minus_decompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/minus_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/eq_add_S.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/expand_mult2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_2.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ring/ArithRing/S_to_plus_one.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ZArith/BinInt/ZL0.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/S_plus.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_n_SO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Marseille/GC/lib_arith/lib_plus/plus_O_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eqO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_O_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/plus_eqO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/g0.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/McCarthy/g.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_SO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/mult_SO.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack1.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ackermann/Ack.var
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult2_recompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_1.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_O.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_comm.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc_reverse.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/square_recompose.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_sym.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_permut.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_assoc_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_l.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_eq.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_sym.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_permute.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Float/Faux/minus_inv_lt_aux.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_minus_distr_r.con
+WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult_minus_distr_l.con
+Error: Tactic error: No Applicable theorem