X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Ftests%2Fbad_tests%2Fauto.log;h=0cac60da334790dbad4051c260f1dde434e405a7;hb=be5869cd0bbe16c8a67827723c97d2d4fce4c0bc;hp=1e1fc77ae1080b07bb13084035417b93e52f0730;hpb=ceb977d9f052e99b0e473c5484578eaaf307a4f6;p=helm.git

diff --git a/helm/matita/tests/bad_tests/auto.log b/helm/matita/tests/bad_tests/auto.log
index 1e1fc77ae..0cac60da3 100644
--- a/helm/matita/tests/bad_tests/auto.log
+++ b/helm/matita/tests/bad_tests/auto.log
@@ -1,13 +1,6 @@
 Info:  execution of auto.ma started:
 Debug: Executing: ``set "baseuri" "cic:/matita/tests/auto/"''
-Debug: Executing: ``include coq.ma''
-Debug: Executing: ``alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
-Debug: Executing: ``alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xp ...''
-Debug: Executing: ``alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind# ...''
-Debug: Executing: ``alias symbol "eq" (instance 0) = "Coq's leibnitz's ...''
-Debug: Executing: ``alias symbol "minus" (instance 0) = "Coq's natural ...''
-Debug: Executing: ``alias symbol "plus" (instance 0) = "Coq's natural  ...''
-Debug: Executing: ``alias symbol "times" (instance 0) = "Coq's natural ...''
+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