...

[helm.git] / helm / matita / tests / bad_tests / auto.log

diff --git a/helm/matita/tests/bad_tests/auto.log b/helm/matita/tests/bad_tests/auto.log
index 1e1fc77ae1080b07bb13084035417b93e52f0730..a66efc52d9d5dc2263dd51937504f5529628a17f 100644 (file)
--- a/helm/matita/tests/bad_tests/auto.log
+++ b/helm/matita/tests/bad_tests/auto.log
@@ -1,13 +1,6 @@
 \e[0;32mInfo:  \e[0mexecution of auto.ma started:
 \e[0;34mDebug: \e[0mExecuting: ``set "baseuri" "cic:/matita/tests/auto/"''
-\e[0;34mDebug: \e[0mExecuting: ``include coq.ma''
-\e[0;34mDebug: \e[0mExecuting: ``alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
-\e[0;34mDebug: \e[0mExecuting: ``alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
-\e[0;34mDebug: \e[0mExecuting: ``alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind# ...''
-\e[0;34mDebug: \e[0mExecuting: ``alias symbol "eq" (instance 0) = "Coq's leibnitz's ...''
-\e[0;34mDebug: \e[0mExecuting: ``alias symbol "minus" (instance 0) = "Coq's natural ...''
-\e[0;34mDebug: \e[0mExecuting: ``alias symbol "plus" (instance 0) = "Coq's natural  ...''
-\e[0;34mDebug: \e[0mExecuting: ``alias symbol "times" (instance 0) = "Coq's natural ...''
+\e[0;34mDebug: \e[0mExecuting: ``include cic:/Coq''
 \e[0;34mDebug: \e[0mExecuting: ``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