From: Claudio Sacerdoti Coen Date: Wed, 18 Jan 2006 12:20:41 +0000 (+0000) Subject: baseuri of coq.ma fixed X-Git-Tag: make_still_working~7818 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3aeca350068456256c8eadb7b1784909e238b79f;p=helm.git baseuri of coq.ma fixed --- diff --git a/helm/matita/library/legacy/coq.ma b/helm/matita/library/legacy/coq.ma index ea1f5935d..d3c74fe21 100644 --- a/helm/matita/library/legacy/coq.ma +++ b/helm/matita/library/legacy/coq.ma @@ -1,4 +1,18 @@ -set "baseuri" "cic:/matita/legacy/". +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/legacy/coq/". (* aritmetic operators *) diff --git a/helm/matita/tests/bad_tests/auto.log b/helm/matita/tests/bad_tests/auto.log index a66efc52d..0cac60da3 100644 --- a/helm/matita/tests/bad_tests/auto.log +++ b/helm/matita/tests/bad_tests/auto.log @@ -1,6 +1,6 @@ Info: execution of auto.ma started: Debug: Executing: ``set "baseuri" "cic:/matita/tests/auto/"'' -Debug: Executing: ``include cic:/Coq'' +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