helm/matita/tests/bad_tests/auto.log

   1 \e[0;32mInfo:  \e[0mexecution of auto.ma started:
   2 \e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/auto/"''
   3 \e[0;34mDebug: \e[0mExecuting: ``include coq.ma''
   4 \e[0;34mDebug: \e[0mExecuting: ``alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
   5 \e[0;34mDebug: \e[0mExecuting: ``alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
   6 \e[0;34mDebug: \e[0mExecuting: ``alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind# ...''
   7 \e[0;34mDebug: \e[0mExecuting: ``alias symbol "eq" (instance 0) = "Coq's leibnitz's ...''
   8 \e[0;34mDebug: \e[0mExecuting: ``alias symbol "minus" (instance 0) = "Coq's natural ...''
   9 \e[0;34mDebug: \e[0mExecuting: ``alias symbol "plus" (instance 0) = "Coq's natural  ...''
  10 \e[0;34mDebug: \e[0mExecuting: ``alias symbol "times" (instance 0) = "Coq's natural ...''
  11 \e[0;34mDebug: \e[0mExecuting: ``Theorem a: @[\forall ((x): (@[nat])).(\forall ((y) ...''
  12 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Datatypes/nat.ind
  13 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/eq.ind
  14 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/minus.con
  15 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus.con
  16 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult.con
  17 \e[0;31mError: \e[0mBad name: a
  18 \e[0;34mDebug: \e[0mExecuting: ``intro.''
  19 \e[0;34mDebug: \e[0mExecuting: ``auto.''
  20 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/trans_eq.con
  21 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var
  22 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var
  23 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var
  24 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/z.var
  25 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal3.con
  26 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal2.con
  27 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/f_equal.con
  28 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/B.var
  29 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Logic/Logic_lemmas/equality/f.var
  30 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/add_sub_square_identity.con
  31 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_Sm.con
  32 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/semantics/conservation_0_0.con
  33 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/technical_lemma.con
  34 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/ARITH/Chinese/Nat_complements/technical_lemma.con
  35 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/plus_minus.con
  36 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con
  37 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_plus.con
  38 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_minus.con
  39 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_r.con
  40 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_plus_distr_l.con
  41 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_plus_distr_r.con
  42 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_plus_distr2.con
  43 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_n.con
  44 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Minus/minus_n_O.con
  45 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/minus_minus_lem1.con
  46 WE HAVE NO UNIVERSE FILE FOR cic:/Cachan/SMC/mu/Splus_nm.con
  47 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_Sm.con
  48 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_Sn_m.con
  49 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_Snm_nSm.con
  50 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/TreeAutomata/bases/S_plus_l.con
  51 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/mult_reg_l.con
  52 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_reg_l.con
  53 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute_2_in_4.con
  54 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_permute.con
  55 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_comm.con
  56 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc_reverse.con
  57 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_assoc.con
  58 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_r.con
  59 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_plus_reg_l.con
  60 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eq.con
  61 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_permute2.con
  62 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/minus_eq_decompose.con
  63 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/Qpositive/minus_decompose.con
  64 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/minus_eq.con
  65 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/eq_add_S.con
  66 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/expand_mult2.con
  67 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_2.con
  68 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ring/ArithRing/S_to_plus_one.con
  69 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/ZArith/BinInt/ZL0.con
  70 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/S_plus.con
  71 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_n_SO.con
  72 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/plus_n_O.con
  73 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_r.con
  74 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Plus/plus_0_l.con
  75 WE HAVE NO UNIVERSE FILE FOR cic:/Marseille/GC/lib_arith/lib_plus/plus_O_O.con
  76 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/plus_eqO.con
  77 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/plus_O_O.con
  78 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/plus_eqO.con
  79 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/g0.con
  80 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/McCarthy/g.var
  81 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_SO.con
  82 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Bertrand/Misc/mult_SO.con
  83 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack1.con
  84 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/DEMOS/Demo_AutoRewrite/Ackermann/Ack.var
  85 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_r.con
  86 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_1_l.con
  87 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult2_recompose.con
  88 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_n_1.con
  89 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Init/Peano/mult_n_O.con
  90 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_r.con
  91 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_0_l.con
  92 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_comm.con
  93 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc_reverse.con
  94 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_assoc.con
  95 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/square_recompose.con
  96 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_sym.con
  97 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_permut.con
  98 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/mult_assoc_l.con
  99 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_r.con
 100 WE HAVE NO UNIVERSE FILE FOR cic:/Rocq/SUBST/comparith/eq_mult_reg_l.con
 101 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Rsa/MiscRsa/mult_eq.con
 102 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_sym.con
 103 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/HARDWARE/GENE/Arith_compl/mult_permute.con
 104 WE HAVE NO UNIVERSE FILE FOR cic:/Sophia-Antipolis/Float/Faux/minus_inv_lt_aux.con
 105 WE HAVE NO UNIVERSE FILE FOR cic:/Coq/Arith/Mult/mult_minus_distr_r.con
 106 WE HAVE NO UNIVERSE FILE FOR cic:/Nijmegen/QArith/sqrt2/mult_minus_distr_l.con
 107 \e[0;31mError: \e[0mTactic error: No Applicable theorem