From 945477cf2bd4587727fe492b2c31e10bc20ed906 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 21 Dec 2005 18:18:09 +0000 Subject: [PATCH] ... --- helm/matita/tests/bad_tests/auto.log | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/helm/matita/tests/bad_tests/auto.log b/helm/matita/tests/bad_tests/auto.log index 1e1fc77ae..a66efc52d 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:/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 -- 2.39.2