From 73e52492b520deb0e79e75bd47733366e27e278d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Jan 2008 12:58:43 +0000 Subject: [PATCH] dama, tests, legacy ported --- components/content_pres/termContentPres.ml | 2 + components/lexicon/cicNotation.mli | 2 +- matita/legacy/coq.ma | 2 - matita/library/depends | 12 +- matita/matitacLib.ml | 129 ++++++++++-------- matita/tests/TPTP/Veloci/BOO001-1.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO003-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO003-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO004-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO004-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO005-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO005-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO006-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO006-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO009-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO009-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO010-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO010-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO011-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO011-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO012-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO012-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO013-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO013-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO016-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO017-2.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO018-4.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO034-1.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO069-1.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO071-1.p.ma | 2 +- matita/tests/TPTP/Veloci/BOO075-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL004-3.p.ma | 2 +- matita/tests/TPTP/Veloci/COL007-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL008-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL010-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL012-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL013-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL014-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL015-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL016-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL017-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL018-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL021-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL022-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL024-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL025-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL045-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL048-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL050-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL058-2.p.ma | 2 +- matita/tests/TPTP/Veloci/COL058-3.p.ma | 2 +- matita/tests/TPTP/Veloci/COL060-2.p.ma | 2 +- matita/tests/TPTP/Veloci/COL060-3.p.ma | 2 +- matita/tests/TPTP/Veloci/COL061-2.p.ma | 2 +- matita/tests/TPTP/Veloci/COL061-3.p.ma | 2 +- matita/tests/TPTP/Veloci/COL062-2.p.ma | 2 +- matita/tests/TPTP/Veloci/COL062-3.p.ma | 2 +- matita/tests/TPTP/Veloci/COL063-2.p.ma | 2 +- matita/tests/TPTP/Veloci/COL063-3.p.ma | 2 +- matita/tests/TPTP/Veloci/COL063-4.p.ma | 2 +- matita/tests/TPTP/Veloci/COL063-5.p.ma | 2 +- matita/tests/TPTP/Veloci/COL063-6.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-2.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-3.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-4.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-5.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-6.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-7.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-8.p.ma | 2 +- matita/tests/TPTP/Veloci/COL064-9.p.ma | 2 +- matita/tests/TPTP/Veloci/COL083-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL084-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL085-1.p.ma | 2 +- matita/tests/TPTP/Veloci/COL086-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP001-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP001-4.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP010-4.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP011-4.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP012-4.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP022-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP023-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP115-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP116-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP117-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP118-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP136-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP137-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP139-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP141-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP142-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP143-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP144-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP145-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP146-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP149-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP150-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP151-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP152-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP153-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP154-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP155-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP156-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP157-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP158-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP159-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP160-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP161-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP162-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP163-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP168-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP168-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP173-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP174-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP176-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP176-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP182-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP182-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP182-3.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP182-4.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP186-3.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP186-4.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP188-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP188-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP189-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP189-2.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP192-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP206-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP454-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP455-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP456-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP457-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP458-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP459-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP460-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP463-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP467-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP481-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP484-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP485-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP486-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP487-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP488-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP490-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP491-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP492-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP493-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP494-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP495-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP496-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP497-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP498-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP509-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP510-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP511-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP512-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP513-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP514-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP515-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP516-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP517-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP518-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP520-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP541-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP542-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP543-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP544-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP545-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP546-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP547-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP548-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP549-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP550-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP551-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP552-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP556-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP558-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP560-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP561-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP562-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP564-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP565-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP566-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP567-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP568-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP569-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP570-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP572-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP573-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP574-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP576-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP577-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP578-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP580-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP581-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP582-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP583-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP584-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP586-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP588-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP590-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP592-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP595-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP596-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP597-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP598-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP599-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP600-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP602-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP603-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP604-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP605-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP606-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP608-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP612-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP613-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP614-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP615-1.p.ma | 2 +- matita/tests/TPTP/Veloci/GRP616-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LAT008-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LAT033-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LAT034-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LAT039-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LAT039-2.p.ma | 2 +- matita/tests/TPTP/Veloci/LAT040-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LAT045-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL110-2.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL112-2.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL113-2.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL114-2.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL115-2.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL132-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL133-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL134-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL135-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL139-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL140-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL141-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL153-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL154-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL155-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL156-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL157-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL158-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL161-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LCL164-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LDA001-1.p.ma | 2 +- matita/tests/TPTP/Veloci/LDA007-3.p.ma | 2 +- matita/tests/TPTP/Veloci/RNG007-4.p.ma | 2 +- matita/tests/TPTP/Veloci/RNG008-4.p.ma | 2 +- matita/tests/TPTP/Veloci/RNG011-5.p.ma | 2 +- matita/tests/TPTP/Veloci/RNG023-6.p.ma | 2 +- matita/tests/TPTP/Veloci/RNG023-7.p.ma | 2 +- matita/tests/TPTP/Veloci/RNG024-6.p.ma | 2 +- matita/tests/TPTP/Veloci/RNG024-7.p.ma | 2 +- matita/tests/TPTP/Veloci/ROB002-1.p.ma | 2 +- matita/tests/TPTP/Veloci/ROB009-1.p.ma | 2 +- matita/tests/TPTP/Veloci/ROB010-1.p.ma | 2 +- matita/tests/TPTP/Veloci/ROB013-1.p.ma | 2 +- matita/tests/TPTP/Veloci/ROB030-1.p.ma | 2 +- matita/tests/TPTP/Veloci/SYN083-1.p.ma | 2 +- matita/tests/absurd.ma | 4 +- matita/tests/apply.ma | 4 +- matita/tests/apply2.ma | 2 +- matita/tests/applys.ma | 2 +- matita/tests/assumption.ma | 4 +- matita/tests/bad_induction.ma | 2 +- matita/tests/bad_tests/auto.ma | 4 +- matita/tests/bad_tests/baseuri.ma | 4 +- matita/tests/bool.ma | 4 +- matita/tests/change.ma | 4 +- matita/tests/clear.ma | 4 +- matita/tests/clearbody.ma | 4 +- matita/tests/coercions.ma | 2 +- matita/tests/coercions_contravariant.ma | 8 +- matita/tests/coercions_dependent.ma | 4 +- matita/tests/coercions_dupelim.ma | 2 +- matita/tests/coercions_nonuniform.ma | 10 +- matita/tests/coercions_open.ma | 8 +- matita/tests/coercions_propagation.ma | 12 +- matita/tests/coercions_russell.ma | 16 +-- matita/tests/comments.ma | 4 +- matita/tests/compose.ma | 2 +- matita/tests/constructor.ma | 4 +- matita/tests/continuationals.ma | 4 +- matita/tests/contradiction.ma | 4 +- matita/tests/cut.ma | 4 +- matita/tests/decl.ma | 2 +- matita/tests/decompose.ma | 2 +- matita/tests/demodulation_coq.ma | 4 +- matita/tests/demodulation_matita.ma | 2 +- matita/tests/dependent_injection.ma | 4 +- matita/tests/dependent_type_inference.ma | 2 +- matita/tests/destruct.ma | 2 +- matita/tests/elim.ma | 4 +- matita/tests/fguidi.ma | 6 +- matita/tests/first.ma | 2 +- matita/tests/fix_betareduction.ma | 4 +- matita/tests/fold.ma | 4 +- matita/tests/generalize.ma | 4 +- matita/tests/hard_refine.ma | 4 +- matita/tests/injection.ma | 4 +- .../tests/interactive/automatic_insertion.ma | 2 +- matita/tests/interactive/drop.ma | 2 +- matita/tests/interactive/grafite.ma | 2 +- matita/tests/interactive/test5.ma | 2 +- matita/tests/interactive/test6.ma | 2 +- matita/tests/interactive/test7.ma | 2 +- matita/tests/interactive/test_instance.ma | 2 +- matita/tests/inversion.ma | 4 +- matita/tests/inversion2.ma | 4 +- matita/tests/letrec.ma | 2 +- matita/tests/letrecand.ma | 2 +- matita/tests/match_inference.ma | 2 +- matita/tests/metasenv_ordering.ma | 4 +- matita/tests/multiple_inheritance.ma | 4 +- matita/tests/mysql_escaping.ma | 2 +- matita/tests/naiveparamod.ma | 2 +- matita/tests/overred.ma | 6 +- matita/tests/paramodulation.ma | 4 +- matita/tests/paramodulation/BOO075-1.ma | 26 ++-- .../tests/paramodulation/boolean_algebra.ma | 4 +- matita/tests/paramodulation/group.ma | 4 +- matita/tests/paramodulation/irratsqrt2.ma | 2 +- matita/tests/pullback.ma | 2 +- matita/tests/record.ma | 2 +- matita/tests/replace.ma | 4 +- matita/tests/rewrite.ma | 4 +- matita/tests/second.ma | 2 +- matita/tests/simpl.ma | 4 +- matita/tests/tacticals.ma | 2 +- matita/tests/test2.ma | 4 +- matita/tests/test3.ma | 4 +- matita/tests/test4.ma | 4 +- matita/tests/third.ma | 2 +- matita/tests/tinycals.ma | 2 +- matita/tests/unfold.ma | 4 +- 336 files changed, 486 insertions(+), 473 deletions(-) diff --git a/components/content_pres/termContentPres.ml b/components/content_pres/termContentPres.ml index 0ee424f18..2fccd4f64 100644 --- a/components/content_pres/termContentPres.ml +++ b/components/content_pres/termContentPres.ml @@ -672,3 +672,5 @@ let instantiate_level2 env term = let _ = load_patterns21 [] + + diff --git a/components/lexicon/cicNotation.mli b/components/lexicon/cicNotation.mli index 944438df8..00b34babe 100644 --- a/components/lexicon/cicNotation.mli +++ b/components/lexicon/cicNotation.mli @@ -30,7 +30,7 @@ val process_notation: LexiconAst.command -> notation_id list val remove_notation: notation_id -> unit (** {2 Notation enabling/disabling} - * Right now, only disabling of notation during pretty printing is supporting. + * Right now, only disabling of notation during pretty printing is supported. * If it is useful to disable it also for the input phase is still to be * understood ... *) diff --git a/matita/legacy/coq.ma b/matita/legacy/coq.ma index 4ea9919f1..649b866d8 100644 --- a/matita/legacy/coq.ma +++ b/matita/legacy/coq.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/legacy/coq/". - default "equality" cic:/Coq/Init/Logic/eq.ind cic:/Coq/Init/Logic/sym_eq.con diff --git a/matita/library/depends b/matita/library/depends index 40cddf02f..da550394a 100644 --- a/matita/library/depends +++ b/matita/library/depends @@ -2,7 +2,7 @@ library_notation.ma Q/q.ma Z/compare.ma Z/orders.ma Z/plus.ma Z/times.ma Z/z.ma Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma Z/moebius.ma Z/sigma_p.ma nat/factorization.ma Z/times.ma Z/plus.ma nat/lt_arith.ma -Z/orders.ma logic/connectives.ma Z/z.ma nat/orders.ma +Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma Z/plus.ma Z/z.ma nat/minus.ma Z/compare.ma Z/orders.ma nat/compare.ma @@ -16,8 +16,8 @@ assembly/extra.ma list/list.ma nat/div_and_mod.ma nat/primes.ma datatypes/constructors.ma logic/equality.ma datatypes/compare.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma -algebra/groups.ma logic/connectives.ma algebra/monoids.ma datatypes/bool.ma nat/compare.ma nat/le_arith.ma -algebra/finite_groups.ma nat/relevant_equations.ma algebra/groups.ma +algebra/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma +algebra/finite_groups.ma algebra/groups.ma nat/relevant_equations.ma algebra/semigroups.ma higher_order_defs/functions.ma algebra/monoids.ma algebra/semigroups.ma algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma @@ -25,10 +25,10 @@ algebra/CoRN/SemiGroups.ma algebra/CoRN/SetoidInc.ma algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma algebra/CoRN/SetoidFun.ma algebra/CoRN/Setoids.ma higher_order_defs/relations.ma demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma -demo/power_derivative.ma nat/nat.ma nat/compare.ma nat/orders.ma nat/plus.ma +demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma list/sort.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma list/list.ma higher_order_defs/functions.ma logic/equality.ma nat/nat.ma -logic/equality.ma logic/connectives.ma higher_order_defs/relations.ma +logic/equality.ma higher_order_defs/relations.ma logic/connectives.ma logic/connectives.ma logic/coimplication.ma logic/connectives.ma logic/connectives2.ma higher_order_defs/relations.ma @@ -64,7 +64,7 @@ nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma nat/nat.ma higher_order_defs/functions.ma nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma nat/map_iter_p.ma nat/count.ma nat/permutation.ma -nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma +nat/orders.ma higher_order_defs/ordering.ma logic/connectives.ma nat/nat.ma nat/pi_p.ma nat/generic_iter_p.ma nat/iteration2.ma nat/primes.ma nat/plus.ma nat/nat.ma nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma diff --git a/matita/matitacLib.ml b/matita/matitacLib.ml index a17845331..51834f6e7 100644 --- a/matita/matitacLib.ml +++ b/matita/matitacLib.ml @@ -29,7 +29,7 @@ open Printf open GrafiteTypes -exception AttemptToInsertAnAlias +exception AttemptToInsertAnAlias of LexiconEngine.status let out = ref ignore let set_callback f = out := f @@ -108,59 +108,58 @@ let get_include_paths options = ;; let rec compile options fname = - (* initialization, MOVE OUTSIDE *) let matita_debug = Helm_registry.get_bool "matita.debug" in - (* sanity checks *) let include_paths = get_include_paths options in let root,baseuri,fname,_tgt = Librarian.baseuri_of_script ~include_paths fname in - let moo_fname = - LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true - in - let lexicon_fname= - LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true - in - if Http_getter_storage.is_read_only baseuri then - HLog.error - (Printf.sprintf "uri %s belongs to a read-only repository" baseuri); - (* cleanup of previously compiled objects *) - if (not (Http_getter_storage.is_empty ~local:true baseuri) || - LibraryClean.db_uris_of_baseuri baseuri <> []) - then begin - HLog.message ("baseuri " ^ baseuri ^ " is not empty"); - HLog.message ("cleaning baseuri " ^ baseuri); - LibraryClean.clean_baseuris [baseuri]; - assert (Http_getter_storage.is_empty ~local:true baseuri); - end; - (* create dir for XML files *) - if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" - ~default:false) - then - HExtlib.mkdir - (Filename.dirname - (Http_getter.filename ~local:true ~writable:true (baseuri ^ - "foo.con"))); - (* begin of compilation *) let grafite_status = GrafiteSync.init baseuri in let lexicon_status = CicNotation2.load_notation ~include_paths:[] BuildTimeConf.core_notation_script in + let initial_lexicon_status = lexicon_status in let big_bang = Unix.gettimeofday () in let time = Unix.time () in - HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri); - if not (Helm_registry.get_bool "matita.verbose") then - (let cc = - if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt" - else "matitac" - in - let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in - print_string s; flush stdout); - let buf = Ulexing.from_utf8_channel (open_in fname) in - let print_cb = - if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ()) - else pp_ast_statement - in try + (* sanity checks *) + let moo_fname = + LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true + in + let lexicon_fname= + LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true + in + if Http_getter_storage.is_read_only baseuri then + HLog.error + (Printf.sprintf "uri %s belongs to a read-only repository" baseuri); + (* cleanup of previously compiled objects *) + if (not (Http_getter_storage.is_empty ~local:true baseuri) || + LibraryClean.db_uris_of_baseuri baseuri <> []) + then begin + HLog.message ("baseuri " ^ baseuri ^ " is not empty"); + HLog.message ("cleaning baseuri " ^ baseuri); + LibraryClean.clean_baseuris [baseuri]; + assert (Http_getter_storage.is_empty ~local:true baseuri); + end; + (* create dir for XML files *) + if not (Helm_registry.get_opt_default Helm_registry.bool "matita.nodisk" + ~default:false) + then + HExtlib.mkdir + (Filename.dirname + (Http_getter.filename ~local:true ~writable:true (baseuri ^ + "foo.con"))); + HLog.message ("compiling " ^ Filename.basename fname ^ " in " ^ baseuri); + if not (Helm_registry.get_bool "matita.verbose") then + (let cc = + if Str.string_match(Str.regexp ".*opt$") Sys.argv.(0) 0 then "matitac.opt" + else "matitac" + in + let s = Printf.sprintf "%s %-35s " cc (cut (root^"/") fname) in + print_string s; flush stdout); + let buf = Ulexing.from_utf8_channel (open_in fname) in + let print_cb = + if not (Helm_registry.get_bool "matita.verbose") then (fun _ _ -> ()) + else pp_ast_statement + in let grafite_status, lexicon_status = match MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths @@ -168,7 +167,7 @@ let rec compile options fname = with | [] -> raise End_of_file | ((grafite,lexicon),None)::_ -> grafite, lexicon - | (s,Some _)::_ -> raise AttemptToInsertAnAlias + | ((_,l),Some _)::_ -> raise (AttemptToInsertAnAlias l) in let elapsed = Unix.time () -. time in let proof_status,moo_content_rev,lexicon_content_rev = @@ -179,6 +178,7 @@ let rec compile options fname = (HLog.error "there are still incomplete proofs at the end of the script"; pp_times fname false big_bang; + LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; clean_exit baseuri false) else (if Helm_registry.get_bool "matita.moo" then begin @@ -197,26 +197,39 @@ let rec compile options fname = HLog.message (sprintf "execution of %s completed in %s." fname (hou^min^sec)); pp_times fname true big_bang; + LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; true) with - | End_of_file -> HLog.error "End_of_file?!"; clean_exit baseuri false + | End_of_file -> + HLog.error "End_of_file"; + pp_times fname false big_bang; + clean_exit baseuri false + | AttemptToInsertAnAlias lexicon_status -> + pp_times fname false big_bang; + LexiconSync.time_travel ~present:lexicon_status ~past:initial_lexicon_status; + clean_exit baseuri false | Sys.Break as exn -> - if matita_debug then raise exn; + if matita_debug then raise exn; HLog.error "user break!"; pp_times fname false big_bang; clean_exit baseuri false | GrafiteEngine.Macro (floc, f) -> - (match f (get_macro_context (Some grafite_status)) with - | _, GrafiteAst.Inline (_, style, suri, prefix) -> - let str = - ApplyTransformation.txt_of_inline_macro style suri prefix - ~map_unicode_to_tex:(Helm_registry.get_bool - "matita.paste_unicode_as_tex") in - !out str; - compile options fname - | _ -> - let x, y = HExtlib.loc_of_floc floc in - HLog.error (sprintf "A macro has been found at %d-%d" x y); + (try + match f (get_macro_context (Some grafite_status)) with + | _, GrafiteAst.Inline (_, style, suri, prefix) -> + let str = + ApplyTransformation.txt_of_inline_macro style suri prefix + ~map_unicode_to_tex:(Helm_registry.get_bool + "matita.paste_unicode_as_tex") in + !out str; + compile options fname + | _ -> + let x, y = HExtlib.loc_of_floc floc in + HLog.error (sprintf "A macro has been found at %d-%d" x y); + pp_times fname false big_bang; + clean_exit baseuri false + with exn -> + HLog.error (snd (MatitaExcPp.to_string exn)); pp_times fname false big_bang; clean_exit baseuri false) | HExtlib.Localized (floc,CicNotationParser.Parse_error err) -> @@ -225,7 +238,7 @@ let rec compile options fname = pp_times fname false big_bang; clean_exit baseuri false | exn -> - if matita_debug then raise exn; + if matita_debug then raise exn; HLog.error (snd (MatitaExcPp.to_string exn)); pp_times fname false big_bang; clean_exit baseuri false diff --git a/matita/tests/TPTP/Veloci/BOO001-1.p.ma b/matita/tests/TPTP/Veloci/BOO001-1.p.ma index 87ee6a7c5..3cb2beeda 100644 --- a/matita/tests/TPTP/Veloci/BOO001-1.p.ma +++ b/matita/tests/TPTP/Veloci/BOO001-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO001-1". + include "logic/equality.ma". (* Inclusion of: BOO001-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO003-2.p.ma b/matita/tests/TPTP/Veloci/BOO003-2.p.ma index a964a96ad..f41c21a1f 100644 --- a/matita/tests/TPTP/Veloci/BOO003-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO003-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO003-2". + include "logic/equality.ma". (* Inclusion of: BOO003-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO003-4.p.ma b/matita/tests/TPTP/Veloci/BOO003-4.p.ma index efeca0198..a3761dfa7 100644 --- a/matita/tests/TPTP/Veloci/BOO003-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO003-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO003-4". + include "logic/equality.ma". (* Inclusion of: BOO003-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO004-2.p.ma b/matita/tests/TPTP/Veloci/BOO004-2.p.ma index ff3cd85f9..abd4fa54f 100644 --- a/matita/tests/TPTP/Veloci/BOO004-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO004-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO004-2". + include "logic/equality.ma". (* Inclusion of: BOO004-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO004-4.p.ma b/matita/tests/TPTP/Veloci/BOO004-4.p.ma index 1821077fe..d4cc8aa8c 100644 --- a/matita/tests/TPTP/Veloci/BOO004-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO004-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO004-4". + include "logic/equality.ma". (* Inclusion of: BOO004-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO005-2.p.ma b/matita/tests/TPTP/Veloci/BOO005-2.p.ma index 5e3def47c..4ba359aeb 100644 --- a/matita/tests/TPTP/Veloci/BOO005-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO005-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO005-2". + include "logic/equality.ma". (* Inclusion of: BOO005-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO005-4.p.ma b/matita/tests/TPTP/Veloci/BOO005-4.p.ma index 9bd9ce8a9..06363d0c0 100644 --- a/matita/tests/TPTP/Veloci/BOO005-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO005-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO005-4". + include "logic/equality.ma". (* Inclusion of: BOO005-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO006-2.p.ma b/matita/tests/TPTP/Veloci/BOO006-2.p.ma index 77ea2d76b..3091ecaeb 100644 --- a/matita/tests/TPTP/Veloci/BOO006-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO006-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO006-2". + include "logic/equality.ma". (* Inclusion of: BOO006-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO006-4.p.ma b/matita/tests/TPTP/Veloci/BOO006-4.p.ma index c05bd84fc..9eeab88a0 100644 --- a/matita/tests/TPTP/Veloci/BOO006-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO006-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO006-4". + include "logic/equality.ma". (* Inclusion of: BOO006-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO009-2.p.ma b/matita/tests/TPTP/Veloci/BOO009-2.p.ma index ce93dc23b..ac47a7375 100644 --- a/matita/tests/TPTP/Veloci/BOO009-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO009-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO009-2". + include "logic/equality.ma". (* Inclusion of: BOO009-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO009-4.p.ma b/matita/tests/TPTP/Veloci/BOO009-4.p.ma index 67631beb7..00794316a 100644 --- a/matita/tests/TPTP/Veloci/BOO009-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO009-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO009-4". + include "logic/equality.ma". (* Inclusion of: BOO009-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO010-2.p.ma b/matita/tests/TPTP/Veloci/BOO010-2.p.ma index 9517fa3ed..5863f860b 100644 --- a/matita/tests/TPTP/Veloci/BOO010-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO010-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO010-2". + include "logic/equality.ma". (* Inclusion of: BOO010-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO010-4.p.ma b/matita/tests/TPTP/Veloci/BOO010-4.p.ma index 6cd030d5a..0a392b221 100644 --- a/matita/tests/TPTP/Veloci/BOO010-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO010-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO010-4". + include "logic/equality.ma". (* Inclusion of: BOO010-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO011-2.p.ma b/matita/tests/TPTP/Veloci/BOO011-2.p.ma index 33f8f9a87..e9cbcd929 100644 --- a/matita/tests/TPTP/Veloci/BOO011-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO011-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO011-2". + include "logic/equality.ma". (* Inclusion of: BOO011-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO011-4.p.ma b/matita/tests/TPTP/Veloci/BOO011-4.p.ma index 5855e8aee..c61c06d42 100644 --- a/matita/tests/TPTP/Veloci/BOO011-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO011-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO011-4". + include "logic/equality.ma". (* Inclusion of: BOO011-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO012-2.p.ma b/matita/tests/TPTP/Veloci/BOO012-2.p.ma index 3572d8750..40d9d9b53 100644 --- a/matita/tests/TPTP/Veloci/BOO012-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO012-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO012-2". + include "logic/equality.ma". (* Inclusion of: BOO012-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO012-4.p.ma b/matita/tests/TPTP/Veloci/BOO012-4.p.ma index fb67030b9..4c3ad768c 100644 --- a/matita/tests/TPTP/Veloci/BOO012-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO012-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO012-4". + include "logic/equality.ma". (* Inclusion of: BOO012-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO013-2.p.ma b/matita/tests/TPTP/Veloci/BOO013-2.p.ma index 0f538a7da..5dd357b06 100644 --- a/matita/tests/TPTP/Veloci/BOO013-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO013-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO013-2". + include "logic/equality.ma". (* Inclusion of: BOO013-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO013-4.p.ma b/matita/tests/TPTP/Veloci/BOO013-4.p.ma index f4b986a97..2a948d54c 100644 --- a/matita/tests/TPTP/Veloci/BOO013-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO013-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO013-4". + include "logic/equality.ma". (* Inclusion of: BOO013-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO016-2.p.ma b/matita/tests/TPTP/Veloci/BOO016-2.p.ma index ee7c9969c..f096eb8ae 100644 --- a/matita/tests/TPTP/Veloci/BOO016-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO016-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO016-2". + include "logic/equality.ma". (* Inclusion of: BOO016-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO017-2.p.ma b/matita/tests/TPTP/Veloci/BOO017-2.p.ma index 5691fcfb0..95dfd1ba1 100644 --- a/matita/tests/TPTP/Veloci/BOO017-2.p.ma +++ b/matita/tests/TPTP/Veloci/BOO017-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO017-2". + include "logic/equality.ma". (* Inclusion of: BOO017-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO018-4.p.ma b/matita/tests/TPTP/Veloci/BOO018-4.p.ma index 32fe9a460..3c867cf28 100644 --- a/matita/tests/TPTP/Veloci/BOO018-4.p.ma +++ b/matita/tests/TPTP/Veloci/BOO018-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO018-4". + include "logic/equality.ma". (* Inclusion of: BOO018-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO034-1.p.ma b/matita/tests/TPTP/Veloci/BOO034-1.p.ma index adab6c4ae..d4c19b5fb 100644 --- a/matita/tests/TPTP/Veloci/BOO034-1.p.ma +++ b/matita/tests/TPTP/Veloci/BOO034-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO034-1". + include "logic/equality.ma". (* Inclusion of: BOO034-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO069-1.p.ma b/matita/tests/TPTP/Veloci/BOO069-1.p.ma index 38bbe0e44..44559bdea 100644 --- a/matita/tests/TPTP/Veloci/BOO069-1.p.ma +++ b/matita/tests/TPTP/Veloci/BOO069-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO069-1". + include "logic/equality.ma". (* Inclusion of: BOO069-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO071-1.p.ma b/matita/tests/TPTP/Veloci/BOO071-1.p.ma index 1cddbb9ae..b84cf7df2 100644 --- a/matita/tests/TPTP/Veloci/BOO071-1.p.ma +++ b/matita/tests/TPTP/Veloci/BOO071-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO071-1". + include "logic/equality.ma". (* Inclusion of: BOO071-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/BOO075-1.p.ma b/matita/tests/TPTP/Veloci/BOO075-1.p.ma index 971fa231a..ae56431c7 100644 --- a/matita/tests/TPTP/Veloci/BOO075-1.p.ma +++ b/matita/tests/TPTP/Veloci/BOO075-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO075-1". + include "logic/equality.ma". (* Inclusion of: BOO075-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL004-3.p.ma b/matita/tests/TPTP/Veloci/COL004-3.p.ma index f9a7712ee..e982e3513 100644 --- a/matita/tests/TPTP/Veloci/COL004-3.p.ma +++ b/matita/tests/TPTP/Veloci/COL004-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL004-3". + include "logic/equality.ma". (* Inclusion of: COL004-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL007-1.p.ma b/matita/tests/TPTP/Veloci/COL007-1.p.ma index 655b2a2ce..b5c637281 100644 --- a/matita/tests/TPTP/Veloci/COL007-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL007-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL007-1". + include "logic/equality.ma". (* Inclusion of: COL007-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL008-1.p.ma b/matita/tests/TPTP/Veloci/COL008-1.p.ma index a3ff086db..0e9db587e 100644 --- a/matita/tests/TPTP/Veloci/COL008-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL008-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL008-1". + include "logic/equality.ma". (* Inclusion of: COL008-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL010-1.p.ma b/matita/tests/TPTP/Veloci/COL010-1.p.ma index 45bd7de31..421552442 100644 --- a/matita/tests/TPTP/Veloci/COL010-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL010-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL010-1". + include "logic/equality.ma". (* Inclusion of: COL010-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL012-1.p.ma b/matita/tests/TPTP/Veloci/COL012-1.p.ma index 866be5178..58b5de1f3 100644 --- a/matita/tests/TPTP/Veloci/COL012-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL012-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL012-1". + include "logic/equality.ma". (* Inclusion of: COL012-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL013-1.p.ma b/matita/tests/TPTP/Veloci/COL013-1.p.ma index 07d594e3c..d6290447f 100644 --- a/matita/tests/TPTP/Veloci/COL013-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL013-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL013-1". + include "logic/equality.ma". (* Inclusion of: COL013-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL014-1.p.ma b/matita/tests/TPTP/Veloci/COL014-1.p.ma index 6e618736a..5f92c04ba 100644 --- a/matita/tests/TPTP/Veloci/COL014-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL014-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL014-1". + include "logic/equality.ma". (* Inclusion of: COL014-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL015-1.p.ma b/matita/tests/TPTP/Veloci/COL015-1.p.ma index fcff6921c..2d77c6c6f 100644 --- a/matita/tests/TPTP/Veloci/COL015-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL015-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL015-1". + include "logic/equality.ma". (* Inclusion of: COL015-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL016-1.p.ma b/matita/tests/TPTP/Veloci/COL016-1.p.ma index 37a3765cb..4da683f9a 100644 --- a/matita/tests/TPTP/Veloci/COL016-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL016-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL016-1". + include "logic/equality.ma". (* Inclusion of: COL016-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL017-1.p.ma b/matita/tests/TPTP/Veloci/COL017-1.p.ma index 36d03e6e5..62f30c7a0 100644 --- a/matita/tests/TPTP/Veloci/COL017-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL017-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL017-1". + include "logic/equality.ma". (* Inclusion of: COL017-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL018-1.p.ma b/matita/tests/TPTP/Veloci/COL018-1.p.ma index e218bae4a..325fde8ce 100644 --- a/matita/tests/TPTP/Veloci/COL018-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL018-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL018-1". + include "logic/equality.ma". (* Inclusion of: COL018-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL021-1.p.ma b/matita/tests/TPTP/Veloci/COL021-1.p.ma index e8f9c3579..4b809bd6e 100644 --- a/matita/tests/TPTP/Veloci/COL021-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL021-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL021-1". + include "logic/equality.ma". (* Inclusion of: COL021-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL022-1.p.ma b/matita/tests/TPTP/Veloci/COL022-1.p.ma index a311f146f..183ea8551 100644 --- a/matita/tests/TPTP/Veloci/COL022-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL022-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL022-1". + include "logic/equality.ma". (* Inclusion of: COL022-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL024-1.p.ma b/matita/tests/TPTP/Veloci/COL024-1.p.ma index c38e40574..a779158ba 100644 --- a/matita/tests/TPTP/Veloci/COL024-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL024-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL024-1". + include "logic/equality.ma". (* Inclusion of: COL024-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL025-1.p.ma b/matita/tests/TPTP/Veloci/COL025-1.p.ma index a7fa25856..46b622eb5 100644 --- a/matita/tests/TPTP/Veloci/COL025-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL025-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL025-1". + include "logic/equality.ma". (* Inclusion of: COL025-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL045-1.p.ma b/matita/tests/TPTP/Veloci/COL045-1.p.ma index df48469b0..5863d6ffd 100644 --- a/matita/tests/TPTP/Veloci/COL045-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL045-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL045-1". + include "logic/equality.ma". (* Inclusion of: COL045-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL048-1.p.ma b/matita/tests/TPTP/Veloci/COL048-1.p.ma index a0435b2c2..deb4006f5 100644 --- a/matita/tests/TPTP/Veloci/COL048-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL048-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL048-1". + include "logic/equality.ma". (* Inclusion of: COL048-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL050-1.p.ma b/matita/tests/TPTP/Veloci/COL050-1.p.ma index 10f25dc2a..e8383c1b1 100644 --- a/matita/tests/TPTP/Veloci/COL050-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL050-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL050-1". + include "logic/equality.ma". (* Inclusion of: COL050-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL058-2.p.ma b/matita/tests/TPTP/Veloci/COL058-2.p.ma index 5b216a3d2..b109ddc68 100644 --- a/matita/tests/TPTP/Veloci/COL058-2.p.ma +++ b/matita/tests/TPTP/Veloci/COL058-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL058-2". + include "logic/equality.ma". (* Inclusion of: COL058-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL058-3.p.ma b/matita/tests/TPTP/Veloci/COL058-3.p.ma index 2235cb57d..b5ed2f6ad 100644 --- a/matita/tests/TPTP/Veloci/COL058-3.p.ma +++ b/matita/tests/TPTP/Veloci/COL058-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL058-3". + include "logic/equality.ma". (* Inclusion of: COL058-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL060-2.p.ma b/matita/tests/TPTP/Veloci/COL060-2.p.ma index da151819a..3dcfb651e 100644 --- a/matita/tests/TPTP/Veloci/COL060-2.p.ma +++ b/matita/tests/TPTP/Veloci/COL060-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL060-2". + include "logic/equality.ma". (* Inclusion of: COL060-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL060-3.p.ma b/matita/tests/TPTP/Veloci/COL060-3.p.ma index d1ff7bc9b..202a46864 100644 --- a/matita/tests/TPTP/Veloci/COL060-3.p.ma +++ b/matita/tests/TPTP/Veloci/COL060-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL060-3". + include "logic/equality.ma". (* Inclusion of: COL060-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL061-2.p.ma b/matita/tests/TPTP/Veloci/COL061-2.p.ma index 81adc265d..e85df51f3 100644 --- a/matita/tests/TPTP/Veloci/COL061-2.p.ma +++ b/matita/tests/TPTP/Veloci/COL061-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL061-2". + include "logic/equality.ma". (* Inclusion of: COL061-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL061-3.p.ma b/matita/tests/TPTP/Veloci/COL061-3.p.ma index 0359b3ce9..aa80c3f36 100644 --- a/matita/tests/TPTP/Veloci/COL061-3.p.ma +++ b/matita/tests/TPTP/Veloci/COL061-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL061-3". + include "logic/equality.ma". (* Inclusion of: COL061-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL062-2.p.ma b/matita/tests/TPTP/Veloci/COL062-2.p.ma index 383a285e8..48ff2a903 100644 --- a/matita/tests/TPTP/Veloci/COL062-2.p.ma +++ b/matita/tests/TPTP/Veloci/COL062-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL062-2". + include "logic/equality.ma". (* Inclusion of: COL062-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL062-3.p.ma b/matita/tests/TPTP/Veloci/COL062-3.p.ma index 8b65e0c4f..b335f6908 100644 --- a/matita/tests/TPTP/Veloci/COL062-3.p.ma +++ b/matita/tests/TPTP/Veloci/COL062-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL062-3". + include "logic/equality.ma". (* Inclusion of: COL062-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL063-2.p.ma b/matita/tests/TPTP/Veloci/COL063-2.p.ma index 02f91ef49..2050c35cd 100644 --- a/matita/tests/TPTP/Veloci/COL063-2.p.ma +++ b/matita/tests/TPTP/Veloci/COL063-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL063-2". + include "logic/equality.ma". (* Inclusion of: COL063-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL063-3.p.ma b/matita/tests/TPTP/Veloci/COL063-3.p.ma index 70205ee89..8e5671ae3 100644 --- a/matita/tests/TPTP/Veloci/COL063-3.p.ma +++ b/matita/tests/TPTP/Veloci/COL063-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL063-3". + include "logic/equality.ma". (* Inclusion of: COL063-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL063-4.p.ma b/matita/tests/TPTP/Veloci/COL063-4.p.ma index 38bb35318..bf6fdb5b7 100644 --- a/matita/tests/TPTP/Veloci/COL063-4.p.ma +++ b/matita/tests/TPTP/Veloci/COL063-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL063-4". + include "logic/equality.ma". (* Inclusion of: COL063-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL063-5.p.ma b/matita/tests/TPTP/Veloci/COL063-5.p.ma index 4c98273b5..35d1a0c48 100644 --- a/matita/tests/TPTP/Veloci/COL063-5.p.ma +++ b/matita/tests/TPTP/Veloci/COL063-5.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL063-5". + include "logic/equality.ma". (* Inclusion of: COL063-5.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL063-6.p.ma b/matita/tests/TPTP/Veloci/COL063-6.p.ma index 19fbd39fa..608ba68ab 100644 --- a/matita/tests/TPTP/Veloci/COL063-6.p.ma +++ b/matita/tests/TPTP/Veloci/COL063-6.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL063-6". + include "logic/equality.ma". (* Inclusion of: COL063-6.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-2.p.ma b/matita/tests/TPTP/Veloci/COL064-2.p.ma index 4e6d8af15..5bdab285a 100644 --- a/matita/tests/TPTP/Veloci/COL064-2.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-2". + include "logic/equality.ma". (* Inclusion of: COL064-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-3.p.ma b/matita/tests/TPTP/Veloci/COL064-3.p.ma index 5644d38c1..898040321 100644 --- a/matita/tests/TPTP/Veloci/COL064-3.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-3". + include "logic/equality.ma". (* Inclusion of: COL064-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-4.p.ma b/matita/tests/TPTP/Veloci/COL064-4.p.ma index 34fbe9349..d964987e1 100644 --- a/matita/tests/TPTP/Veloci/COL064-4.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-4". + include "logic/equality.ma". (* Inclusion of: COL064-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-5.p.ma b/matita/tests/TPTP/Veloci/COL064-5.p.ma index 414887588..9ea160cdb 100644 --- a/matita/tests/TPTP/Veloci/COL064-5.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-5.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-5". + include "logic/equality.ma". (* Inclusion of: COL064-5.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-6.p.ma b/matita/tests/TPTP/Veloci/COL064-6.p.ma index 4d054e035..b2e7fad83 100644 --- a/matita/tests/TPTP/Veloci/COL064-6.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-6.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-6". + include "logic/equality.ma". (* Inclusion of: COL064-6.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-7.p.ma b/matita/tests/TPTP/Veloci/COL064-7.p.ma index 1c3ddc2f2..a1a903e80 100644 --- a/matita/tests/TPTP/Veloci/COL064-7.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-7.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-7". + include "logic/equality.ma". (* Inclusion of: COL064-7.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-8.p.ma b/matita/tests/TPTP/Veloci/COL064-8.p.ma index 120a6d047..1a72e8482 100644 --- a/matita/tests/TPTP/Veloci/COL064-8.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-8.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-8". + include "logic/equality.ma". (* Inclusion of: COL064-8.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL064-9.p.ma b/matita/tests/TPTP/Veloci/COL064-9.p.ma index 07591bb4c..521947e4d 100644 --- a/matita/tests/TPTP/Veloci/COL064-9.p.ma +++ b/matita/tests/TPTP/Veloci/COL064-9.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL064-9". + include "logic/equality.ma". (* Inclusion of: COL064-9.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL083-1.p.ma b/matita/tests/TPTP/Veloci/COL083-1.p.ma index 89d991761..5580a76cc 100644 --- a/matita/tests/TPTP/Veloci/COL083-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL083-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL083-1". + include "logic/equality.ma". (* Inclusion of: COL083-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL084-1.p.ma b/matita/tests/TPTP/Veloci/COL084-1.p.ma index 4d2d057bc..8813fc43b 100644 --- a/matita/tests/TPTP/Veloci/COL084-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL084-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL084-1". + include "logic/equality.ma". (* Inclusion of: COL084-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL085-1.p.ma b/matita/tests/TPTP/Veloci/COL085-1.p.ma index 7fd4279ce..0e0cac71b 100644 --- a/matita/tests/TPTP/Veloci/COL085-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL085-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL085-1". + include "logic/equality.ma". (* Inclusion of: COL085-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/COL086-1.p.ma b/matita/tests/TPTP/Veloci/COL086-1.p.ma index e4527c48b..2fce42e46 100644 --- a/matita/tests/TPTP/Veloci/COL086-1.p.ma +++ b/matita/tests/TPTP/Veloci/COL086-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/COL086-1". + include "logic/equality.ma". (* Inclusion of: COL086-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP001-2.p.ma b/matita/tests/TPTP/Veloci/GRP001-2.p.ma index d4e79c748..07a012a4a 100644 --- a/matita/tests/TPTP/Veloci/GRP001-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP001-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP001-2". + include "logic/equality.ma". (* Inclusion of: GRP001-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP001-4.p.ma b/matita/tests/TPTP/Veloci/GRP001-4.p.ma index 544eaf116..01683bfdf 100644 --- a/matita/tests/TPTP/Veloci/GRP001-4.p.ma +++ b/matita/tests/TPTP/Veloci/GRP001-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP001-4". + include "logic/equality.ma". (* Inclusion of: GRP001-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP010-4.p.ma b/matita/tests/TPTP/Veloci/GRP010-4.p.ma index b6a3f51c1..a7a94c741 100644 --- a/matita/tests/TPTP/Veloci/GRP010-4.p.ma +++ b/matita/tests/TPTP/Veloci/GRP010-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP010-4". + include "logic/equality.ma". (* Inclusion of: GRP010-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP011-4.p.ma b/matita/tests/TPTP/Veloci/GRP011-4.p.ma index 6391656ba..a935ade1c 100644 --- a/matita/tests/TPTP/Veloci/GRP011-4.p.ma +++ b/matita/tests/TPTP/Veloci/GRP011-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP011-4". + include "logic/equality.ma". (* Inclusion of: GRP011-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP012-4.p.ma b/matita/tests/TPTP/Veloci/GRP012-4.p.ma index ed5338825..067a3f7de 100644 --- a/matita/tests/TPTP/Veloci/GRP012-4.p.ma +++ b/matita/tests/TPTP/Veloci/GRP012-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP012-4". + include "logic/equality.ma". (* Inclusion of: GRP012-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP022-2.p.ma b/matita/tests/TPTP/Veloci/GRP022-2.p.ma index db2519fe6..a87fe3a57 100644 --- a/matita/tests/TPTP/Veloci/GRP022-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP022-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP022-2". + include "logic/equality.ma". (* Inclusion of: GRP022-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP023-2.p.ma b/matita/tests/TPTP/Veloci/GRP023-2.p.ma index 4ad352201..c1a22f39a 100644 --- a/matita/tests/TPTP/Veloci/GRP023-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP023-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP023-2". + include "logic/equality.ma". (* Inclusion of: GRP023-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP115-1.p.ma b/matita/tests/TPTP/Veloci/GRP115-1.p.ma index 6c605ee94..e6fed36fa 100644 --- a/matita/tests/TPTP/Veloci/GRP115-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP115-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP115-1". + include "logic/equality.ma". (* Inclusion of: GRP115-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP116-1.p.ma b/matita/tests/TPTP/Veloci/GRP116-1.p.ma index 3cc4b5719..25e483f3b 100644 --- a/matita/tests/TPTP/Veloci/GRP116-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP116-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP116-1". + include "logic/equality.ma". (* Inclusion of: GRP116-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP117-1.p.ma b/matita/tests/TPTP/Veloci/GRP117-1.p.ma index 8768d0eab..31fcdf4bb 100644 --- a/matita/tests/TPTP/Veloci/GRP117-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP117-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP117-1". + include "logic/equality.ma". (* Inclusion of: GRP117-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP118-1.p.ma b/matita/tests/TPTP/Veloci/GRP118-1.p.ma index 4d01353ea..aeb184a1e 100644 --- a/matita/tests/TPTP/Veloci/GRP118-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP118-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP118-1". + include "logic/equality.ma". (* Inclusion of: GRP118-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP136-1.p.ma b/matita/tests/TPTP/Veloci/GRP136-1.p.ma index e108ae55b..091644967 100644 --- a/matita/tests/TPTP/Veloci/GRP136-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP136-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP136-1". + include "logic/equality.ma". (* Inclusion of: GRP136-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP137-1.p.ma b/matita/tests/TPTP/Veloci/GRP137-1.p.ma index 322702cc5..6d1b6b2a0 100644 --- a/matita/tests/TPTP/Veloci/GRP137-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP137-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP137-1". + include "logic/equality.ma". (* Inclusion of: GRP137-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP139-1.p.ma b/matita/tests/TPTP/Veloci/GRP139-1.p.ma index cf868c306..1752d8580 100644 --- a/matita/tests/TPTP/Veloci/GRP139-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP139-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP139-1". + include "logic/equality.ma". (* Inclusion of: GRP139-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP141-1.p.ma b/matita/tests/TPTP/Veloci/GRP141-1.p.ma index 3706a25d7..84e880f7a 100644 --- a/matita/tests/TPTP/Veloci/GRP141-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP141-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP141-1". + include "logic/equality.ma". (* Inclusion of: GRP141-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP142-1.p.ma b/matita/tests/TPTP/Veloci/GRP142-1.p.ma index 1f13705e1..a8dfa8d6f 100644 --- a/matita/tests/TPTP/Veloci/GRP142-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP142-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP142-1". + include "logic/equality.ma". (* Inclusion of: GRP142-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP143-1.p.ma b/matita/tests/TPTP/Veloci/GRP143-1.p.ma index be00186ae..c32dac6b7 100644 --- a/matita/tests/TPTP/Veloci/GRP143-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP143-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP143-1". + include "logic/equality.ma". (* Inclusion of: GRP143-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP144-1.p.ma b/matita/tests/TPTP/Veloci/GRP144-1.p.ma index be20f1901..1ffa96eeb 100644 --- a/matita/tests/TPTP/Veloci/GRP144-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP144-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP144-1". + include "logic/equality.ma". (* Inclusion of: GRP144-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP145-1.p.ma b/matita/tests/TPTP/Veloci/GRP145-1.p.ma index 032cdfd55..fb0233e25 100644 --- a/matita/tests/TPTP/Veloci/GRP145-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP145-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP145-1". + include "logic/equality.ma". (* Inclusion of: GRP145-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP146-1.p.ma b/matita/tests/TPTP/Veloci/GRP146-1.p.ma index 6bacee188..ee91a7e45 100644 --- a/matita/tests/TPTP/Veloci/GRP146-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP146-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP146-1". + include "logic/equality.ma". (* Inclusion of: GRP146-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP149-1.p.ma b/matita/tests/TPTP/Veloci/GRP149-1.p.ma index e6c7d4ff6..bcc3de3be 100644 --- a/matita/tests/TPTP/Veloci/GRP149-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP149-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP149-1". + include "logic/equality.ma". (* Inclusion of: GRP149-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP150-1.p.ma b/matita/tests/TPTP/Veloci/GRP150-1.p.ma index f612ede8e..569788972 100644 --- a/matita/tests/TPTP/Veloci/GRP150-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP150-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP150-1". + include "logic/equality.ma". (* Inclusion of: GRP150-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP151-1.p.ma b/matita/tests/TPTP/Veloci/GRP151-1.p.ma index 240c266b2..d08424625 100644 --- a/matita/tests/TPTP/Veloci/GRP151-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP151-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP151-1". + include "logic/equality.ma". (* Inclusion of: GRP151-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP152-1.p.ma b/matita/tests/TPTP/Veloci/GRP152-1.p.ma index d9078e5fb..f795a6412 100644 --- a/matita/tests/TPTP/Veloci/GRP152-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP152-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP152-1". + include "logic/equality.ma". (* Inclusion of: GRP152-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP153-1.p.ma b/matita/tests/TPTP/Veloci/GRP153-1.p.ma index 7dc86aa7e..e6abb3997 100644 --- a/matita/tests/TPTP/Veloci/GRP153-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP153-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP153-1". + include "logic/equality.ma". (* Inclusion of: GRP153-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP154-1.p.ma b/matita/tests/TPTP/Veloci/GRP154-1.p.ma index 51832886c..501deedf7 100644 --- a/matita/tests/TPTP/Veloci/GRP154-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP154-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP154-1". + include "logic/equality.ma". (* Inclusion of: GRP154-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP155-1.p.ma b/matita/tests/TPTP/Veloci/GRP155-1.p.ma index 7a940e531..42503caae 100644 --- a/matita/tests/TPTP/Veloci/GRP155-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP155-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP155-1". + include "logic/equality.ma". (* Inclusion of: GRP155-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP156-1.p.ma b/matita/tests/TPTP/Veloci/GRP156-1.p.ma index 544290f56..fcb186c2a 100644 --- a/matita/tests/TPTP/Veloci/GRP156-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP156-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP156-1". + include "logic/equality.ma". (* Inclusion of: GRP156-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP157-1.p.ma b/matita/tests/TPTP/Veloci/GRP157-1.p.ma index 63868e1bf..3f1fe8911 100644 --- a/matita/tests/TPTP/Veloci/GRP157-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP157-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP157-1". + include "logic/equality.ma". (* Inclusion of: GRP157-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP158-1.p.ma b/matita/tests/TPTP/Veloci/GRP158-1.p.ma index 710c30a1b..f156eaec4 100644 --- a/matita/tests/TPTP/Veloci/GRP158-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP158-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP158-1". + include "logic/equality.ma". (* Inclusion of: GRP158-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP159-1.p.ma b/matita/tests/TPTP/Veloci/GRP159-1.p.ma index ca0b0ffdf..752911c3d 100644 --- a/matita/tests/TPTP/Veloci/GRP159-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP159-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP159-1". + include "logic/equality.ma". (* Inclusion of: GRP159-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP160-1.p.ma b/matita/tests/TPTP/Veloci/GRP160-1.p.ma index 1d49bcea1..2a98c44ae 100644 --- a/matita/tests/TPTP/Veloci/GRP160-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP160-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP160-1". + include "logic/equality.ma". (* Inclusion of: GRP160-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP161-1.p.ma b/matita/tests/TPTP/Veloci/GRP161-1.p.ma index ff4878fbc..b96a0d70a 100644 --- a/matita/tests/TPTP/Veloci/GRP161-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP161-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP161-1". + include "logic/equality.ma". (* Inclusion of: GRP161-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP162-1.p.ma b/matita/tests/TPTP/Veloci/GRP162-1.p.ma index 4d4fa4e5e..b5b33a25a 100644 --- a/matita/tests/TPTP/Veloci/GRP162-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP162-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP162-1". + include "logic/equality.ma". (* Inclusion of: GRP162-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP163-1.p.ma b/matita/tests/TPTP/Veloci/GRP163-1.p.ma index 3065332b9..e9dfaebaf 100644 --- a/matita/tests/TPTP/Veloci/GRP163-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP163-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP163-1". + include "logic/equality.ma". (* Inclusion of: GRP163-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP168-1.p.ma b/matita/tests/TPTP/Veloci/GRP168-1.p.ma index 905257851..59bd4a635 100644 --- a/matita/tests/TPTP/Veloci/GRP168-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP168-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP168-1". + include "logic/equality.ma". (* Inclusion of: GRP168-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP168-2.p.ma b/matita/tests/TPTP/Veloci/GRP168-2.p.ma index 8e6697270..d575e4366 100644 --- a/matita/tests/TPTP/Veloci/GRP168-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP168-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP168-2". + include "logic/equality.ma". (* Inclusion of: GRP168-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP173-1.p.ma b/matita/tests/TPTP/Veloci/GRP173-1.p.ma index d6b61595c..9f5b22b10 100644 --- a/matita/tests/TPTP/Veloci/GRP173-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP173-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP173-1". + include "logic/equality.ma". (* Inclusion of: GRP173-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP174-1.p.ma b/matita/tests/TPTP/Veloci/GRP174-1.p.ma index bd8fecc10..b08649ba6 100644 --- a/matita/tests/TPTP/Veloci/GRP174-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP174-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP174-1". + include "logic/equality.ma". (* Inclusion of: GRP174-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP176-1.p.ma b/matita/tests/TPTP/Veloci/GRP176-1.p.ma index fe03f9f02..28e992d2d 100644 --- a/matita/tests/TPTP/Veloci/GRP176-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP176-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP176-1". + include "logic/equality.ma". (* Inclusion of: GRP176-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP176-2.p.ma b/matita/tests/TPTP/Veloci/GRP176-2.p.ma index 153ac5806..73db9743a 100644 --- a/matita/tests/TPTP/Veloci/GRP176-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP176-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP176-2". + include "logic/equality.ma". (* Inclusion of: GRP176-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP182-1.p.ma b/matita/tests/TPTP/Veloci/GRP182-1.p.ma index b2166c28f..68c61f9f4 100644 --- a/matita/tests/TPTP/Veloci/GRP182-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP182-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP182-1". + include "logic/equality.ma". (* Inclusion of: GRP182-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP182-2.p.ma b/matita/tests/TPTP/Veloci/GRP182-2.p.ma index f8955ab0e..ba9ab8705 100644 --- a/matita/tests/TPTP/Veloci/GRP182-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP182-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP182-2". + include "logic/equality.ma". (* Inclusion of: GRP182-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP182-3.p.ma b/matita/tests/TPTP/Veloci/GRP182-3.p.ma index fa4e6ce23..744ad2e04 100644 --- a/matita/tests/TPTP/Veloci/GRP182-3.p.ma +++ b/matita/tests/TPTP/Veloci/GRP182-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP182-3". + include "logic/equality.ma". (* Inclusion of: GRP182-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP182-4.p.ma b/matita/tests/TPTP/Veloci/GRP182-4.p.ma index 95fb312fb..7c11b0fa4 100644 --- a/matita/tests/TPTP/Veloci/GRP182-4.p.ma +++ b/matita/tests/TPTP/Veloci/GRP182-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP182-4". + include "logic/equality.ma". (* Inclusion of: GRP182-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP186-3.p.ma b/matita/tests/TPTP/Veloci/GRP186-3.p.ma index a39543178..a2fd0a9eb 100644 --- a/matita/tests/TPTP/Veloci/GRP186-3.p.ma +++ b/matita/tests/TPTP/Veloci/GRP186-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP186-3". + include "logic/equality.ma". (* Inclusion of: GRP186-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP186-4.p.ma b/matita/tests/TPTP/Veloci/GRP186-4.p.ma index be8354b19..421da6945 100644 --- a/matita/tests/TPTP/Veloci/GRP186-4.p.ma +++ b/matita/tests/TPTP/Veloci/GRP186-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP186-4". + include "logic/equality.ma". (* Inclusion of: GRP186-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP188-1.p.ma b/matita/tests/TPTP/Veloci/GRP188-1.p.ma index da64fdee3..7ca52046b 100644 --- a/matita/tests/TPTP/Veloci/GRP188-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP188-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP188-1". + include "logic/equality.ma". (* Inclusion of: GRP188-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP188-2.p.ma b/matita/tests/TPTP/Veloci/GRP188-2.p.ma index 771056e01..c9dc85905 100644 --- a/matita/tests/TPTP/Veloci/GRP188-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP188-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP188-2". + include "logic/equality.ma". (* Inclusion of: GRP188-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP189-1.p.ma b/matita/tests/TPTP/Veloci/GRP189-1.p.ma index 183e7b772..4978c31d2 100644 --- a/matita/tests/TPTP/Veloci/GRP189-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP189-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP189-1". + include "logic/equality.ma". (* Inclusion of: GRP189-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP189-2.p.ma b/matita/tests/TPTP/Veloci/GRP189-2.p.ma index 0b47a1614..b36fa01a9 100644 --- a/matita/tests/TPTP/Veloci/GRP189-2.p.ma +++ b/matita/tests/TPTP/Veloci/GRP189-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP189-2". + include "logic/equality.ma". (* Inclusion of: GRP189-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP192-1.p.ma b/matita/tests/TPTP/Veloci/GRP192-1.p.ma index 01ca783b0..f7b77e363 100644 --- a/matita/tests/TPTP/Veloci/GRP192-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP192-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP192-1". + include "logic/equality.ma". (* Inclusion of: GRP192-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP206-1.p.ma b/matita/tests/TPTP/Veloci/GRP206-1.p.ma index 9c5b5bcce..08544742a 100644 --- a/matita/tests/TPTP/Veloci/GRP206-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP206-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP206-1". + include "logic/equality.ma". (* Inclusion of: GRP206-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP454-1.p.ma b/matita/tests/TPTP/Veloci/GRP454-1.p.ma index 257fdd49a..d0d0b9ce0 100644 --- a/matita/tests/TPTP/Veloci/GRP454-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP454-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP454-1". + include "logic/equality.ma". (* Inclusion of: GRP454-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP455-1.p.ma b/matita/tests/TPTP/Veloci/GRP455-1.p.ma index deaa9a2f0..5a981ed5a 100644 --- a/matita/tests/TPTP/Veloci/GRP455-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP455-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP455-1". + include "logic/equality.ma". (* Inclusion of: GRP455-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP456-1.p.ma b/matita/tests/TPTP/Veloci/GRP456-1.p.ma index 228a4f3a6..c9787c2c5 100644 --- a/matita/tests/TPTP/Veloci/GRP456-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP456-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP456-1". + include "logic/equality.ma". (* Inclusion of: GRP456-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP457-1.p.ma b/matita/tests/TPTP/Veloci/GRP457-1.p.ma index acd2050d2..1bb70c158 100644 --- a/matita/tests/TPTP/Veloci/GRP457-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP457-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP457-1". + include "logic/equality.ma". (* Inclusion of: GRP457-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP458-1.p.ma b/matita/tests/TPTP/Veloci/GRP458-1.p.ma index 44091f50e..f3a52a241 100644 --- a/matita/tests/TPTP/Veloci/GRP458-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP458-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP458-1". + include "logic/equality.ma". (* Inclusion of: GRP458-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP459-1.p.ma b/matita/tests/TPTP/Veloci/GRP459-1.p.ma index 303f73741..7c717aac6 100644 --- a/matita/tests/TPTP/Veloci/GRP459-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP459-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP459-1". + include "logic/equality.ma". (* Inclusion of: GRP459-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP460-1.p.ma b/matita/tests/TPTP/Veloci/GRP460-1.p.ma index 698ac8a23..c97120d43 100644 --- a/matita/tests/TPTP/Veloci/GRP460-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP460-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP460-1". + include "logic/equality.ma". (* Inclusion of: GRP460-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP463-1.p.ma b/matita/tests/TPTP/Veloci/GRP463-1.p.ma index fcd04c0c5..31e130867 100644 --- a/matita/tests/TPTP/Veloci/GRP463-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP463-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP463-1". + include "logic/equality.ma". (* Inclusion of: GRP463-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP467-1.p.ma b/matita/tests/TPTP/Veloci/GRP467-1.p.ma index 1107f4b98..8b295b557 100644 --- a/matita/tests/TPTP/Veloci/GRP467-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP467-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP467-1". + include "logic/equality.ma". (* Inclusion of: GRP467-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP481-1.p.ma b/matita/tests/TPTP/Veloci/GRP481-1.p.ma index bf063d591..af2dbb515 100644 --- a/matita/tests/TPTP/Veloci/GRP481-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP481-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP481-1". + include "logic/equality.ma". (* Inclusion of: GRP481-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP484-1.p.ma b/matita/tests/TPTP/Veloci/GRP484-1.p.ma index e8588f917..ae8efa8b6 100644 --- a/matita/tests/TPTP/Veloci/GRP484-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP484-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP484-1". + include "logic/equality.ma". (* Inclusion of: GRP484-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP485-1.p.ma b/matita/tests/TPTP/Veloci/GRP485-1.p.ma index 2a015e13e..77afd17a3 100644 --- a/matita/tests/TPTP/Veloci/GRP485-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP485-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP485-1". + include "logic/equality.ma". (* Inclusion of: GRP485-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP486-1.p.ma b/matita/tests/TPTP/Veloci/GRP486-1.p.ma index ccdaf0ea9..1517c62d8 100644 --- a/matita/tests/TPTP/Veloci/GRP486-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP486-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP486-1". + include "logic/equality.ma". (* Inclusion of: GRP486-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP487-1.p.ma b/matita/tests/TPTP/Veloci/GRP487-1.p.ma index a26acef17..83a1864cf 100644 --- a/matita/tests/TPTP/Veloci/GRP487-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP487-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP487-1". + include "logic/equality.ma". (* Inclusion of: GRP487-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP488-1.p.ma b/matita/tests/TPTP/Veloci/GRP488-1.p.ma index ff1c3c177..b588912d9 100644 --- a/matita/tests/TPTP/Veloci/GRP488-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP488-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP488-1". + include "logic/equality.ma". (* Inclusion of: GRP488-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP490-1.p.ma b/matita/tests/TPTP/Veloci/GRP490-1.p.ma index 78e958798..32e96c095 100644 --- a/matita/tests/TPTP/Veloci/GRP490-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP490-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP490-1". + include "logic/equality.ma". (* Inclusion of: GRP490-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP491-1.p.ma b/matita/tests/TPTP/Veloci/GRP491-1.p.ma index 221fdb592..a3bfcd369 100644 --- a/matita/tests/TPTP/Veloci/GRP491-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP491-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP491-1". + include "logic/equality.ma". (* Inclusion of: GRP491-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP492-1.p.ma b/matita/tests/TPTP/Veloci/GRP492-1.p.ma index e9f198d2d..c353c8dd4 100644 --- a/matita/tests/TPTP/Veloci/GRP492-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP492-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP492-1". + include "logic/equality.ma". (* Inclusion of: GRP492-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP493-1.p.ma b/matita/tests/TPTP/Veloci/GRP493-1.p.ma index fc0bf16ce..b3b6e1113 100644 --- a/matita/tests/TPTP/Veloci/GRP493-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP493-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP493-1". + include "logic/equality.ma". (* Inclusion of: GRP493-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP494-1.p.ma b/matita/tests/TPTP/Veloci/GRP494-1.p.ma index ea863067a..d731521ca 100644 --- a/matita/tests/TPTP/Veloci/GRP494-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP494-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP494-1". + include "logic/equality.ma". (* Inclusion of: GRP494-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP495-1.p.ma b/matita/tests/TPTP/Veloci/GRP495-1.p.ma index 225028412..376a7fb3e 100644 --- a/matita/tests/TPTP/Veloci/GRP495-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP495-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP495-1". + include "logic/equality.ma". (* Inclusion of: GRP495-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP496-1.p.ma b/matita/tests/TPTP/Veloci/GRP496-1.p.ma index efe2d3a94..6116704e9 100644 --- a/matita/tests/TPTP/Veloci/GRP496-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP496-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP496-1". + include "logic/equality.ma". (* Inclusion of: GRP496-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP497-1.p.ma b/matita/tests/TPTP/Veloci/GRP497-1.p.ma index c2f5d7be9..2f36dfcea 100644 --- a/matita/tests/TPTP/Veloci/GRP497-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP497-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP497-1". + include "logic/equality.ma". (* Inclusion of: GRP497-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP498-1.p.ma b/matita/tests/TPTP/Veloci/GRP498-1.p.ma index c5875b0b2..a838cf615 100644 --- a/matita/tests/TPTP/Veloci/GRP498-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP498-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP498-1". + include "logic/equality.ma". (* Inclusion of: GRP498-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP509-1.p.ma b/matita/tests/TPTP/Veloci/GRP509-1.p.ma index 25618b46a..633a5eb89 100644 --- a/matita/tests/TPTP/Veloci/GRP509-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP509-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP509-1". + include "logic/equality.ma". (* Inclusion of: GRP509-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP510-1.p.ma b/matita/tests/TPTP/Veloci/GRP510-1.p.ma index 1003a4014..2c054d9fa 100644 --- a/matita/tests/TPTP/Veloci/GRP510-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP510-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP510-1". + include "logic/equality.ma". (* Inclusion of: GRP510-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP511-1.p.ma b/matita/tests/TPTP/Veloci/GRP511-1.p.ma index ff8c9f4c0..9a25b0d9b 100644 --- a/matita/tests/TPTP/Veloci/GRP511-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP511-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP511-1". + include "logic/equality.ma". (* Inclusion of: GRP511-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP512-1.p.ma b/matita/tests/TPTP/Veloci/GRP512-1.p.ma index 19a8c4a94..fa17d9922 100644 --- a/matita/tests/TPTP/Veloci/GRP512-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP512-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP512-1". + include "logic/equality.ma". (* Inclusion of: GRP512-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP513-1.p.ma b/matita/tests/TPTP/Veloci/GRP513-1.p.ma index 03409c949..c5f734d01 100644 --- a/matita/tests/TPTP/Veloci/GRP513-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP513-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP513-1". + include "logic/equality.ma". (* Inclusion of: GRP513-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP514-1.p.ma b/matita/tests/TPTP/Veloci/GRP514-1.p.ma index 90593b6c8..7fde98484 100644 --- a/matita/tests/TPTP/Veloci/GRP514-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP514-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP514-1". + include "logic/equality.ma". (* Inclusion of: GRP514-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP515-1.p.ma b/matita/tests/TPTP/Veloci/GRP515-1.p.ma index 7b526ef97..489631234 100644 --- a/matita/tests/TPTP/Veloci/GRP515-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP515-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP515-1". + include "logic/equality.ma". (* Inclusion of: GRP515-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP516-1.p.ma b/matita/tests/TPTP/Veloci/GRP516-1.p.ma index af15eb7ee..15a873c65 100644 --- a/matita/tests/TPTP/Veloci/GRP516-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP516-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP516-1". + include "logic/equality.ma". (* Inclusion of: GRP516-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP517-1.p.ma b/matita/tests/TPTP/Veloci/GRP517-1.p.ma index a488717cd..e4a0a13d6 100644 --- a/matita/tests/TPTP/Veloci/GRP517-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP517-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP517-1". + include "logic/equality.ma". (* Inclusion of: GRP517-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP518-1.p.ma b/matita/tests/TPTP/Veloci/GRP518-1.p.ma index a953ab610..7c5ef76cc 100644 --- a/matita/tests/TPTP/Veloci/GRP518-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP518-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP518-1". + include "logic/equality.ma". (* Inclusion of: GRP518-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP520-1.p.ma b/matita/tests/TPTP/Veloci/GRP520-1.p.ma index ea992df71..3c5f1a9b5 100644 --- a/matita/tests/TPTP/Veloci/GRP520-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP520-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP520-1". + include "logic/equality.ma". (* Inclusion of: GRP520-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP541-1.p.ma b/matita/tests/TPTP/Veloci/GRP541-1.p.ma index a8f428a0d..7f9233193 100644 --- a/matita/tests/TPTP/Veloci/GRP541-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP541-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP541-1". + include "logic/equality.ma". (* Inclusion of: GRP541-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP542-1.p.ma b/matita/tests/TPTP/Veloci/GRP542-1.p.ma index 848748d87..d144c114b 100644 --- a/matita/tests/TPTP/Veloci/GRP542-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP542-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP542-1". + include "logic/equality.ma". (* Inclusion of: GRP542-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP543-1.p.ma b/matita/tests/TPTP/Veloci/GRP543-1.p.ma index cfc5bab58..5fe948ea6 100644 --- a/matita/tests/TPTP/Veloci/GRP543-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP543-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP543-1". + include "logic/equality.ma". (* Inclusion of: GRP543-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP544-1.p.ma b/matita/tests/TPTP/Veloci/GRP544-1.p.ma index 96fb69f73..ffaeb374f 100644 --- a/matita/tests/TPTP/Veloci/GRP544-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP544-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP544-1". + include "logic/equality.ma". (* Inclusion of: GRP544-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP545-1.p.ma b/matita/tests/TPTP/Veloci/GRP545-1.p.ma index 302fb8916..523a17259 100644 --- a/matita/tests/TPTP/Veloci/GRP545-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP545-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP545-1". + include "logic/equality.ma". (* Inclusion of: GRP545-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP546-1.p.ma b/matita/tests/TPTP/Veloci/GRP546-1.p.ma index 2488a9484..b4de2a169 100644 --- a/matita/tests/TPTP/Veloci/GRP546-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP546-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP546-1". + include "logic/equality.ma". (* Inclusion of: GRP546-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP547-1.p.ma b/matita/tests/TPTP/Veloci/GRP547-1.p.ma index 24ede0fe7..bba8f9f07 100644 --- a/matita/tests/TPTP/Veloci/GRP547-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP547-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP547-1". + include "logic/equality.ma". (* Inclusion of: GRP547-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP548-1.p.ma b/matita/tests/TPTP/Veloci/GRP548-1.p.ma index a065d3f1b..be679cf9b 100644 --- a/matita/tests/TPTP/Veloci/GRP548-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP548-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP548-1". + include "logic/equality.ma". (* Inclusion of: GRP548-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP549-1.p.ma b/matita/tests/TPTP/Veloci/GRP549-1.p.ma index 0bf4dbf1c..55c6e1f1a 100644 --- a/matita/tests/TPTP/Veloci/GRP549-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP549-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP549-1". + include "logic/equality.ma". (* Inclusion of: GRP549-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP550-1.p.ma b/matita/tests/TPTP/Veloci/GRP550-1.p.ma index a7482f9b5..340171a78 100644 --- a/matita/tests/TPTP/Veloci/GRP550-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP550-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP550-1". + include "logic/equality.ma". (* Inclusion of: GRP550-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP551-1.p.ma b/matita/tests/TPTP/Veloci/GRP551-1.p.ma index 3144369c2..d67a994ea 100644 --- a/matita/tests/TPTP/Veloci/GRP551-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP551-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP551-1". + include "logic/equality.ma". (* Inclusion of: GRP551-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP552-1.p.ma b/matita/tests/TPTP/Veloci/GRP552-1.p.ma index 9a776c962..e3b3324c8 100644 --- a/matita/tests/TPTP/Veloci/GRP552-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP552-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP552-1". + include "logic/equality.ma". (* Inclusion of: GRP552-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP556-1.p.ma b/matita/tests/TPTP/Veloci/GRP556-1.p.ma index f314261a2..4817e4e1b 100644 --- a/matita/tests/TPTP/Veloci/GRP556-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP556-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP556-1". + include "logic/equality.ma". (* Inclusion of: GRP556-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP558-1.p.ma b/matita/tests/TPTP/Veloci/GRP558-1.p.ma index 35670d9cb..da6a12f62 100644 --- a/matita/tests/TPTP/Veloci/GRP558-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP558-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP558-1". + include "logic/equality.ma". (* Inclusion of: GRP558-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP560-1.p.ma b/matita/tests/TPTP/Veloci/GRP560-1.p.ma index 113f49edf..aa3fb6419 100644 --- a/matita/tests/TPTP/Veloci/GRP560-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP560-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP560-1". + include "logic/equality.ma". (* Inclusion of: GRP560-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP561-1.p.ma b/matita/tests/TPTP/Veloci/GRP561-1.p.ma index dc788b109..2ea4db80e 100644 --- a/matita/tests/TPTP/Veloci/GRP561-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP561-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP561-1". + include "logic/equality.ma". (* Inclusion of: GRP561-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP562-1.p.ma b/matita/tests/TPTP/Veloci/GRP562-1.p.ma index 99ea92789..b3160a042 100644 --- a/matita/tests/TPTP/Veloci/GRP562-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP562-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP562-1". + include "logic/equality.ma". (* Inclusion of: GRP562-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP564-1.p.ma b/matita/tests/TPTP/Veloci/GRP564-1.p.ma index 63b1c2d97..b6071cc66 100644 --- a/matita/tests/TPTP/Veloci/GRP564-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP564-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP564-1". + include "logic/equality.ma". (* Inclusion of: GRP564-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP565-1.p.ma b/matita/tests/TPTP/Veloci/GRP565-1.p.ma index ad4f93570..57f5b453d 100644 --- a/matita/tests/TPTP/Veloci/GRP565-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP565-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP565-1". + include "logic/equality.ma". (* Inclusion of: GRP565-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP566-1.p.ma b/matita/tests/TPTP/Veloci/GRP566-1.p.ma index 71a827e47..1307c5f23 100644 --- a/matita/tests/TPTP/Veloci/GRP566-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP566-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP566-1". + include "logic/equality.ma". (* Inclusion of: GRP566-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP567-1.p.ma b/matita/tests/TPTP/Veloci/GRP567-1.p.ma index 6fbd3492b..2ec8690a4 100644 --- a/matita/tests/TPTP/Veloci/GRP567-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP567-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP567-1". + include "logic/equality.ma". (* Inclusion of: GRP567-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP568-1.p.ma b/matita/tests/TPTP/Veloci/GRP568-1.p.ma index 884ed5e5c..1d63a33f3 100644 --- a/matita/tests/TPTP/Veloci/GRP568-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP568-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP568-1". + include "logic/equality.ma". (* Inclusion of: GRP568-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP569-1.p.ma b/matita/tests/TPTP/Veloci/GRP569-1.p.ma index 931c933ba..58f139e4c 100644 --- a/matita/tests/TPTP/Veloci/GRP569-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP569-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP569-1". + include "logic/equality.ma". (* Inclusion of: GRP569-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP570-1.p.ma b/matita/tests/TPTP/Veloci/GRP570-1.p.ma index d6bdbbfc6..a25f40129 100644 --- a/matita/tests/TPTP/Veloci/GRP570-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP570-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP570-1". + include "logic/equality.ma". (* Inclusion of: GRP570-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP572-1.p.ma b/matita/tests/TPTP/Veloci/GRP572-1.p.ma index c3e517cef..9467a1d9b 100644 --- a/matita/tests/TPTP/Veloci/GRP572-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP572-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP572-1". + include "logic/equality.ma". (* Inclusion of: GRP572-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP573-1.p.ma b/matita/tests/TPTP/Veloci/GRP573-1.p.ma index 8076345cc..c45c0e87e 100644 --- a/matita/tests/TPTP/Veloci/GRP573-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP573-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP573-1". + include "logic/equality.ma". (* Inclusion of: GRP573-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP574-1.p.ma b/matita/tests/TPTP/Veloci/GRP574-1.p.ma index e6f9dfcec..d2f51431f 100644 --- a/matita/tests/TPTP/Veloci/GRP574-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP574-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP574-1". + include "logic/equality.ma". (* Inclusion of: GRP574-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP576-1.p.ma b/matita/tests/TPTP/Veloci/GRP576-1.p.ma index aed52d2de..9851667be 100644 --- a/matita/tests/TPTP/Veloci/GRP576-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP576-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP576-1". + include "logic/equality.ma". (* Inclusion of: GRP576-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP577-1.p.ma b/matita/tests/TPTP/Veloci/GRP577-1.p.ma index ad7c58b9e..16f1de1b6 100644 --- a/matita/tests/TPTP/Veloci/GRP577-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP577-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP577-1". + include "logic/equality.ma". (* Inclusion of: GRP577-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP578-1.p.ma b/matita/tests/TPTP/Veloci/GRP578-1.p.ma index 7c9843da7..f1b196450 100644 --- a/matita/tests/TPTP/Veloci/GRP578-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP578-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP578-1". + include "logic/equality.ma". (* Inclusion of: GRP578-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP580-1.p.ma b/matita/tests/TPTP/Veloci/GRP580-1.p.ma index 4d729b995..6bcb954fd 100644 --- a/matita/tests/TPTP/Veloci/GRP580-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP580-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP580-1". + include "logic/equality.ma". (* Inclusion of: GRP580-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP581-1.p.ma b/matita/tests/TPTP/Veloci/GRP581-1.p.ma index d826e2af1..fa1906ded 100644 --- a/matita/tests/TPTP/Veloci/GRP581-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP581-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP581-1". + include "logic/equality.ma". (* Inclusion of: GRP581-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP582-1.p.ma b/matita/tests/TPTP/Veloci/GRP582-1.p.ma index 4c09bb39c..c20b7e4e8 100644 --- a/matita/tests/TPTP/Veloci/GRP582-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP582-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP582-1". + include "logic/equality.ma". (* Inclusion of: GRP582-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP583-1.p.ma b/matita/tests/TPTP/Veloci/GRP583-1.p.ma index fa95c336a..ed4130734 100644 --- a/matita/tests/TPTP/Veloci/GRP583-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP583-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP583-1". + include "logic/equality.ma". (* Inclusion of: GRP583-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP584-1.p.ma b/matita/tests/TPTP/Veloci/GRP584-1.p.ma index db36e336b..84d08821a 100644 --- a/matita/tests/TPTP/Veloci/GRP584-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP584-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP584-1". + include "logic/equality.ma". (* Inclusion of: GRP584-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP586-1.p.ma b/matita/tests/TPTP/Veloci/GRP586-1.p.ma index f38467e27..0cf2ec1db 100644 --- a/matita/tests/TPTP/Veloci/GRP586-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP586-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP586-1". + include "logic/equality.ma". (* Inclusion of: GRP586-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP588-1.p.ma b/matita/tests/TPTP/Veloci/GRP588-1.p.ma index 1d13edfbe..662725950 100644 --- a/matita/tests/TPTP/Veloci/GRP588-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP588-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP588-1". + include "logic/equality.ma". (* Inclusion of: GRP588-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP590-1.p.ma b/matita/tests/TPTP/Veloci/GRP590-1.p.ma index f678b3d83..5d587a0e1 100644 --- a/matita/tests/TPTP/Veloci/GRP590-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP590-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP590-1". + include "logic/equality.ma". (* Inclusion of: GRP590-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP592-1.p.ma b/matita/tests/TPTP/Veloci/GRP592-1.p.ma index 5612e2720..96c9444ca 100644 --- a/matita/tests/TPTP/Veloci/GRP592-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP592-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP592-1". + include "logic/equality.ma". (* Inclusion of: GRP592-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP595-1.p.ma b/matita/tests/TPTP/Veloci/GRP595-1.p.ma index e97f64cd3..7491debbf 100644 --- a/matita/tests/TPTP/Veloci/GRP595-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP595-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP595-1". + include "logic/equality.ma". (* Inclusion of: GRP595-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP596-1.p.ma b/matita/tests/TPTP/Veloci/GRP596-1.p.ma index 1d8e313ac..c12dfe9ac 100644 --- a/matita/tests/TPTP/Veloci/GRP596-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP596-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP596-1". + include "logic/equality.ma". (* Inclusion of: GRP596-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP597-1.p.ma b/matita/tests/TPTP/Veloci/GRP597-1.p.ma index 5923b8e70..df6892318 100644 --- a/matita/tests/TPTP/Veloci/GRP597-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP597-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP597-1". + include "logic/equality.ma". (* Inclusion of: GRP597-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP598-1.p.ma b/matita/tests/TPTP/Veloci/GRP598-1.p.ma index 133ed30f6..2f416fbb0 100644 --- a/matita/tests/TPTP/Veloci/GRP598-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP598-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP598-1". + include "logic/equality.ma". (* Inclusion of: GRP598-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP599-1.p.ma b/matita/tests/TPTP/Veloci/GRP599-1.p.ma index 31716a710..e55bfc443 100644 --- a/matita/tests/TPTP/Veloci/GRP599-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP599-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP599-1". + include "logic/equality.ma". (* Inclusion of: GRP599-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP600-1.p.ma b/matita/tests/TPTP/Veloci/GRP600-1.p.ma index 07535f9bb..f17fdf2cc 100644 --- a/matita/tests/TPTP/Veloci/GRP600-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP600-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP600-1". + include "logic/equality.ma". (* Inclusion of: GRP600-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP602-1.p.ma b/matita/tests/TPTP/Veloci/GRP602-1.p.ma index 620ddb94e..bcb8a0053 100644 --- a/matita/tests/TPTP/Veloci/GRP602-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP602-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP602-1". + include "logic/equality.ma". (* Inclusion of: GRP602-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP603-1.p.ma b/matita/tests/TPTP/Veloci/GRP603-1.p.ma index 6d7b92f84..82144c1f8 100644 --- a/matita/tests/TPTP/Veloci/GRP603-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP603-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP603-1". + include "logic/equality.ma". (* Inclusion of: GRP603-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP604-1.p.ma b/matita/tests/TPTP/Veloci/GRP604-1.p.ma index 9e228851d..811970fd5 100644 --- a/matita/tests/TPTP/Veloci/GRP604-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP604-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP604-1". + include "logic/equality.ma". (* Inclusion of: GRP604-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP605-1.p.ma b/matita/tests/TPTP/Veloci/GRP605-1.p.ma index 89084a07b..5725d6a19 100644 --- a/matita/tests/TPTP/Veloci/GRP605-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP605-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP605-1". + include "logic/equality.ma". (* Inclusion of: GRP605-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP606-1.p.ma b/matita/tests/TPTP/Veloci/GRP606-1.p.ma index 09742e1ac..567592450 100644 --- a/matita/tests/TPTP/Veloci/GRP606-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP606-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP606-1". + include "logic/equality.ma". (* Inclusion of: GRP606-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP608-1.p.ma b/matita/tests/TPTP/Veloci/GRP608-1.p.ma index de5945331..43fd1ed20 100644 --- a/matita/tests/TPTP/Veloci/GRP608-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP608-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP608-1". + include "logic/equality.ma". (* Inclusion of: GRP608-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP612-1.p.ma b/matita/tests/TPTP/Veloci/GRP612-1.p.ma index 3dec26708..c7aa5405b 100644 --- a/matita/tests/TPTP/Veloci/GRP612-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP612-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP612-1". + include "logic/equality.ma". (* Inclusion of: GRP612-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP613-1.p.ma b/matita/tests/TPTP/Veloci/GRP613-1.p.ma index 206e1edcb..2557b85af 100644 --- a/matita/tests/TPTP/Veloci/GRP613-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP613-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP613-1". + include "logic/equality.ma". (* Inclusion of: GRP613-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP614-1.p.ma b/matita/tests/TPTP/Veloci/GRP614-1.p.ma index 203d3f216..27cf8fec1 100644 --- a/matita/tests/TPTP/Veloci/GRP614-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP614-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP614-1". + include "logic/equality.ma". (* Inclusion of: GRP614-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP615-1.p.ma b/matita/tests/TPTP/Veloci/GRP615-1.p.ma index 2fe6234f6..7be06ff72 100644 --- a/matita/tests/TPTP/Veloci/GRP615-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP615-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP615-1". + include "logic/equality.ma". (* Inclusion of: GRP615-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/GRP616-1.p.ma b/matita/tests/TPTP/Veloci/GRP616-1.p.ma index 6649a53d8..762df9925 100644 --- a/matita/tests/TPTP/Veloci/GRP616-1.p.ma +++ b/matita/tests/TPTP/Veloci/GRP616-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/GRP616-1". + include "logic/equality.ma". (* Inclusion of: GRP616-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LAT008-1.p.ma b/matita/tests/TPTP/Veloci/LAT008-1.p.ma index a8ee942e6..de65d6e9c 100644 --- a/matita/tests/TPTP/Veloci/LAT008-1.p.ma +++ b/matita/tests/TPTP/Veloci/LAT008-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LAT008-1". + include "logic/equality.ma". (* Inclusion of: LAT008-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LAT033-1.p.ma b/matita/tests/TPTP/Veloci/LAT033-1.p.ma index e1897a414..9d53a1f55 100644 --- a/matita/tests/TPTP/Veloci/LAT033-1.p.ma +++ b/matita/tests/TPTP/Veloci/LAT033-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LAT033-1". + include "logic/equality.ma". (* Inclusion of: LAT033-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LAT034-1.p.ma b/matita/tests/TPTP/Veloci/LAT034-1.p.ma index 37ce834ab..2ae473b10 100644 --- a/matita/tests/TPTP/Veloci/LAT034-1.p.ma +++ b/matita/tests/TPTP/Veloci/LAT034-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LAT034-1". + include "logic/equality.ma". (* Inclusion of: LAT034-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LAT039-1.p.ma b/matita/tests/TPTP/Veloci/LAT039-1.p.ma index 8ad8654fc..7165bc391 100644 --- a/matita/tests/TPTP/Veloci/LAT039-1.p.ma +++ b/matita/tests/TPTP/Veloci/LAT039-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LAT039-1". + include "logic/equality.ma". (* Inclusion of: LAT039-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LAT039-2.p.ma b/matita/tests/TPTP/Veloci/LAT039-2.p.ma index de4e55ffa..7000124f6 100644 --- a/matita/tests/TPTP/Veloci/LAT039-2.p.ma +++ b/matita/tests/TPTP/Veloci/LAT039-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LAT039-2". + include "logic/equality.ma". (* Inclusion of: LAT039-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LAT040-1.p.ma b/matita/tests/TPTP/Veloci/LAT040-1.p.ma index a4ff6eff6..a9b80b2a2 100644 --- a/matita/tests/TPTP/Veloci/LAT040-1.p.ma +++ b/matita/tests/TPTP/Veloci/LAT040-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LAT040-1". + include "logic/equality.ma". (* Inclusion of: LAT040-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LAT045-1.p.ma b/matita/tests/TPTP/Veloci/LAT045-1.p.ma index 0b58207db..802ed388b 100644 --- a/matita/tests/TPTP/Veloci/LAT045-1.p.ma +++ b/matita/tests/TPTP/Veloci/LAT045-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LAT045-1". + include "logic/equality.ma". (* Inclusion of: LAT045-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL110-2.p.ma b/matita/tests/TPTP/Veloci/LCL110-2.p.ma index 442ce5958..0467eb2a8 100644 --- a/matita/tests/TPTP/Veloci/LCL110-2.p.ma +++ b/matita/tests/TPTP/Veloci/LCL110-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL110-2". + include "logic/equality.ma". (* Inclusion of: LCL110-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL112-2.p.ma b/matita/tests/TPTP/Veloci/LCL112-2.p.ma index 473cf328c..bc5a0af03 100644 --- a/matita/tests/TPTP/Veloci/LCL112-2.p.ma +++ b/matita/tests/TPTP/Veloci/LCL112-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL112-2". + include "logic/equality.ma". (* Inclusion of: LCL112-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL113-2.p.ma b/matita/tests/TPTP/Veloci/LCL113-2.p.ma index c310916a7..6a19126a7 100644 --- a/matita/tests/TPTP/Veloci/LCL113-2.p.ma +++ b/matita/tests/TPTP/Veloci/LCL113-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL113-2". + include "logic/equality.ma". (* Inclusion of: LCL113-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL114-2.p.ma b/matita/tests/TPTP/Veloci/LCL114-2.p.ma index 46cc01727..98042d05f 100644 --- a/matita/tests/TPTP/Veloci/LCL114-2.p.ma +++ b/matita/tests/TPTP/Veloci/LCL114-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL114-2". + include "logic/equality.ma". (* Inclusion of: LCL114-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL115-2.p.ma b/matita/tests/TPTP/Veloci/LCL115-2.p.ma index 158fef7e8..2bce680be 100644 --- a/matita/tests/TPTP/Veloci/LCL115-2.p.ma +++ b/matita/tests/TPTP/Veloci/LCL115-2.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL115-2". + include "logic/equality.ma". (* Inclusion of: LCL115-2.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL132-1.p.ma b/matita/tests/TPTP/Veloci/LCL132-1.p.ma index 330e40369..9705e8af4 100644 --- a/matita/tests/TPTP/Veloci/LCL132-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL132-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL132-1". + include "logic/equality.ma". (* Inclusion of: LCL132-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL133-1.p.ma b/matita/tests/TPTP/Veloci/LCL133-1.p.ma index acd9538be..39de88054 100644 --- a/matita/tests/TPTP/Veloci/LCL133-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL133-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL133-1". + include "logic/equality.ma". (* Inclusion of: LCL133-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL134-1.p.ma b/matita/tests/TPTP/Veloci/LCL134-1.p.ma index d400f7cff..de3321654 100644 --- a/matita/tests/TPTP/Veloci/LCL134-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL134-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL134-1". + include "logic/equality.ma". (* Inclusion of: LCL134-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL135-1.p.ma b/matita/tests/TPTP/Veloci/LCL135-1.p.ma index 9a982d8af..9c7fbd5f8 100644 --- a/matita/tests/TPTP/Veloci/LCL135-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL135-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL135-1". + include "logic/equality.ma". (* Inclusion of: LCL135-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL139-1.p.ma b/matita/tests/TPTP/Veloci/LCL139-1.p.ma index 21a301128..88914ef32 100644 --- a/matita/tests/TPTP/Veloci/LCL139-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL139-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL139-1". + include "logic/equality.ma". (* Inclusion of: LCL139-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL140-1.p.ma b/matita/tests/TPTP/Veloci/LCL140-1.p.ma index c5148d2a8..e701562f9 100644 --- a/matita/tests/TPTP/Veloci/LCL140-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL140-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL140-1". + include "logic/equality.ma". (* Inclusion of: LCL140-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL141-1.p.ma b/matita/tests/TPTP/Veloci/LCL141-1.p.ma index 5f816e926..fb49a5760 100644 --- a/matita/tests/TPTP/Veloci/LCL141-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL141-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL141-1". + include "logic/equality.ma". (* Inclusion of: LCL141-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL153-1.p.ma b/matita/tests/TPTP/Veloci/LCL153-1.p.ma index 827b99214..f23d00e59 100644 --- a/matita/tests/TPTP/Veloci/LCL153-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL153-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL153-1". + include "logic/equality.ma". (* Inclusion of: LCL153-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL154-1.p.ma b/matita/tests/TPTP/Veloci/LCL154-1.p.ma index 169be886a..1d4c41b30 100644 --- a/matita/tests/TPTP/Veloci/LCL154-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL154-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL154-1". + include "logic/equality.ma". (* Inclusion of: LCL154-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL155-1.p.ma b/matita/tests/TPTP/Veloci/LCL155-1.p.ma index d5cb7fb5e..cf915a8a1 100644 --- a/matita/tests/TPTP/Veloci/LCL155-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL155-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL155-1". + include "logic/equality.ma". (* Inclusion of: LCL155-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL156-1.p.ma b/matita/tests/TPTP/Veloci/LCL156-1.p.ma index 3d5df92b6..9390e4be5 100644 --- a/matita/tests/TPTP/Veloci/LCL156-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL156-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL156-1". + include "logic/equality.ma". (* Inclusion of: LCL156-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL157-1.p.ma b/matita/tests/TPTP/Veloci/LCL157-1.p.ma index 97ea2cad9..18c64d538 100644 --- a/matita/tests/TPTP/Veloci/LCL157-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL157-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL157-1". + include "logic/equality.ma". (* Inclusion of: LCL157-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL158-1.p.ma b/matita/tests/TPTP/Veloci/LCL158-1.p.ma index 32a4518b7..e6e04fac4 100644 --- a/matita/tests/TPTP/Veloci/LCL158-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL158-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL158-1". + include "logic/equality.ma". (* Inclusion of: LCL158-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL161-1.p.ma b/matita/tests/TPTP/Veloci/LCL161-1.p.ma index 3961b05d8..090b2a7a5 100644 --- a/matita/tests/TPTP/Veloci/LCL161-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL161-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL161-1". + include "logic/equality.ma". (* Inclusion of: LCL161-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LCL164-1.p.ma b/matita/tests/TPTP/Veloci/LCL164-1.p.ma index 8850280e9..e5bc4b513 100644 --- a/matita/tests/TPTP/Veloci/LCL164-1.p.ma +++ b/matita/tests/TPTP/Veloci/LCL164-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LCL164-1". + include "logic/equality.ma". (* Inclusion of: LCL164-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LDA001-1.p.ma b/matita/tests/TPTP/Veloci/LDA001-1.p.ma index 48e8b32cc..1963dca39 100644 --- a/matita/tests/TPTP/Veloci/LDA001-1.p.ma +++ b/matita/tests/TPTP/Veloci/LDA001-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LDA001-1". + include "logic/equality.ma". (* Inclusion of: LDA001-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/LDA007-3.p.ma b/matita/tests/TPTP/Veloci/LDA007-3.p.ma index 534a5a9fd..1aeda095a 100644 --- a/matita/tests/TPTP/Veloci/LDA007-3.p.ma +++ b/matita/tests/TPTP/Veloci/LDA007-3.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/LDA007-3". + include "logic/equality.ma". (* Inclusion of: LDA007-3.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/RNG007-4.p.ma b/matita/tests/TPTP/Veloci/RNG007-4.p.ma index a9cdabd1d..97fc8aecb 100644 --- a/matita/tests/TPTP/Veloci/RNG007-4.p.ma +++ b/matita/tests/TPTP/Veloci/RNG007-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/RNG007-4". + include "logic/equality.ma". (* Inclusion of: RNG007-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/RNG008-4.p.ma b/matita/tests/TPTP/Veloci/RNG008-4.p.ma index c56142d62..8652ab6d5 100644 --- a/matita/tests/TPTP/Veloci/RNG008-4.p.ma +++ b/matita/tests/TPTP/Veloci/RNG008-4.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/RNG008-4". + include "logic/equality.ma". (* Inclusion of: RNG008-4.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/RNG011-5.p.ma b/matita/tests/TPTP/Veloci/RNG011-5.p.ma index f7df33340..edd9c7110 100644 --- a/matita/tests/TPTP/Veloci/RNG011-5.p.ma +++ b/matita/tests/TPTP/Veloci/RNG011-5.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/RNG011-5". + include "logic/equality.ma". (* Inclusion of: RNG011-5.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/RNG023-6.p.ma b/matita/tests/TPTP/Veloci/RNG023-6.p.ma index e69e40345..aa8f019d7 100644 --- a/matita/tests/TPTP/Veloci/RNG023-6.p.ma +++ b/matita/tests/TPTP/Veloci/RNG023-6.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/RNG023-6". + include "logic/equality.ma". (* Inclusion of: RNG023-6.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/RNG023-7.p.ma b/matita/tests/TPTP/Veloci/RNG023-7.p.ma index 49260d096..63ae3d9a9 100644 --- a/matita/tests/TPTP/Veloci/RNG023-7.p.ma +++ b/matita/tests/TPTP/Veloci/RNG023-7.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/RNG023-7". + include "logic/equality.ma". (* Inclusion of: RNG023-7.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/RNG024-6.p.ma b/matita/tests/TPTP/Veloci/RNG024-6.p.ma index bdb4c04a7..f4282d600 100644 --- a/matita/tests/TPTP/Veloci/RNG024-6.p.ma +++ b/matita/tests/TPTP/Veloci/RNG024-6.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/RNG024-6". + include "logic/equality.ma". (* Inclusion of: RNG024-6.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/RNG024-7.p.ma b/matita/tests/TPTP/Veloci/RNG024-7.p.ma index afb63d9f6..b4d302383 100644 --- a/matita/tests/TPTP/Veloci/RNG024-7.p.ma +++ b/matita/tests/TPTP/Veloci/RNG024-7.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/RNG024-7". + include "logic/equality.ma". (* Inclusion of: RNG024-7.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/ROB002-1.p.ma b/matita/tests/TPTP/Veloci/ROB002-1.p.ma index 81aabc975..aca76f33d 100644 --- a/matita/tests/TPTP/Veloci/ROB002-1.p.ma +++ b/matita/tests/TPTP/Veloci/ROB002-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/ROB002-1". + include "logic/equality.ma". (* Inclusion of: ROB002-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/ROB009-1.p.ma b/matita/tests/TPTP/Veloci/ROB009-1.p.ma index e3e2ad2b4..4dadbbb6a 100644 --- a/matita/tests/TPTP/Veloci/ROB009-1.p.ma +++ b/matita/tests/TPTP/Veloci/ROB009-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/ROB009-1". + include "logic/equality.ma". (* Inclusion of: ROB009-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/ROB010-1.p.ma b/matita/tests/TPTP/Veloci/ROB010-1.p.ma index 76f06f1af..ec3632d11 100644 --- a/matita/tests/TPTP/Veloci/ROB010-1.p.ma +++ b/matita/tests/TPTP/Veloci/ROB010-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/ROB010-1". + include "logic/equality.ma". (* Inclusion of: ROB010-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/ROB013-1.p.ma b/matita/tests/TPTP/Veloci/ROB013-1.p.ma index 3039f3412..44e1bf65c 100644 --- a/matita/tests/TPTP/Veloci/ROB013-1.p.ma +++ b/matita/tests/TPTP/Veloci/ROB013-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/ROB013-1". + include "logic/equality.ma". (* Inclusion of: ROB013-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/TPTP/Veloci/ROB030-1.p.ma b/matita/tests/TPTP/Veloci/ROB030-1.p.ma index 72fe9de94..d7fc2ebc3 100644 --- a/matita/tests/TPTP/Veloci/ROB030-1.p.ma +++ b/matita/tests/TPTP/Veloci/ROB030-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/ROB030-1". + include "logic/equality.ma". (* Inclusion of: ROB030-1.p *) (* ------------------------------------------------------------------------------ *) diff --git a/matita/tests/TPTP/Veloci/SYN083-1.p.ma b/matita/tests/TPTP/Veloci/SYN083-1.p.ma index c8ac354f0..85efba55e 100644 --- a/matita/tests/TPTP/Veloci/SYN083-1.p.ma +++ b/matita/tests/TPTP/Veloci/SYN083-1.p.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/SYN083-1". + include "logic/equality.ma". (* Inclusion of: SYN083-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/absurd.ma b/matita/tests/absurd.ma index 3a9719e41..9499b63e2 100644 --- a/matita/tests/absurd.ma +++ b/matita/tests/absurd.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/absurd/". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "not" = "cic:/Coq/Init/Logic/not.con". diff --git a/matita/tests/apply.ma b/matita/tests/apply.ma index a77c99ca1..7295a73b5 100644 --- a/matita/tests/apply.ma +++ b/matita/tests/apply.ma @@ -13,8 +13,8 @@ (**************************************************************************) (* test _with_ the WHD on the apply argument *) -set "baseuri" "cic:/matita/tests/apply/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". diff --git a/matita/tests/apply2.ma b/matita/tests/apply2.ma index db87636d7..1d0198fcb 100644 --- a/matita/tests/apply2.ma +++ b/matita/tests/apply2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/apply2". + include "nat/nat.ma". diff --git a/matita/tests/applys.ma b/matita/tests/applys.ma index a26594613..fa0d36998 100644 --- a/matita/tests/applys.ma +++ b/matita/tests/applys.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/applys". + include "nat/div_and_mod.ma". include "nat/factorial.ma". diff --git a/matita/tests/assumption.ma b/matita/tests/assumption.ma index 4b7859e6b..9128f20c6 100644 --- a/matita/tests/assumption.ma +++ b/matita/tests/assumption.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/assumption". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "Coq natural number". diff --git a/matita/tests/bad_induction.ma b/matita/tests/bad_induction.ma index b009e18d1..172aa8e11 100644 --- a/matita/tests/bad_induction.ma +++ b/matita/tests/bad_induction.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/bad_induction". + include "nat/nat.ma". diff --git a/matita/tests/bad_tests/auto.ma b/matita/tests/bad_tests/auto.ma index 2972bfa62..35a2496e6 100755 --- a/matita/tests/bad_tests/auto.ma +++ b/matita/tests/bad_tests/auto.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/auto/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". diff --git a/matita/tests/bad_tests/baseuri.ma b/matita/tests/bad_tests/baseuri.ma index 0e06223fa..127de8565 100644 --- a/matita/tests/bad_tests/baseuri.ma +++ b/matita/tests/bad_tests/baseuri.ma @@ -12,5 +12,5 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/baseuri/". -set "baseuri" "cic:/matita/tests/baseuri/". + + diff --git a/matita/tests/bool.ma b/matita/tests/bool.ma index fe39c310f..3318b74cd 100644 --- a/matita/tests/bool.ma +++ b/matita/tests/bool.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/bool/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". diff --git a/matita/tests/change.ma b/matita/tests/change.ma index 214d0fbe3..fca6c846d 100644 --- a/matita/tests/change.ma +++ b/matita/tests/change.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/change/". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "Coq natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/matita/tests/clear.ma b/matita/tests/clear.ma index 617965258..25c1b64f2 100644 --- a/matita/tests/clear.ma +++ b/matita/tests/clear.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/clear". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". diff --git a/matita/tests/clearbody.ma b/matita/tests/clearbody.ma index 3c95a8a1f..bac472d67 100644 --- a/matita/tests/clearbody.ma +++ b/matita/tests/clearbody.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/clearbody". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "Coq natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/matita/tests/coercions.ma b/matita/tests/coercions.ma index ca8c4abab..e9026af33 100644 --- a/matita/tests/coercions.ma +++ b/matita/tests/coercions.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/coercions/". + include "nat/compare.ma". include "nat/times.ma". diff --git a/matita/tests/coercions_contravariant.ma b/matita/tests/coercions_contravariant.ma index 64f85ea75..153c295c5 100644 --- a/matita/tests/coercions_contravariant.ma +++ b/matita/tests/coercions_contravariant.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/". + include "logic/equality.ma". include "nat/nat.ma". @@ -26,8 +26,8 @@ axiom d : ∀n,m. B n -> B1 m. axiom f : ∀n,m. A n -> B m. axiom g : ∀n.B n. -coercion cic:/matita/test/c.con. -coercion cic:/matita/test/d.con. +coercion cic:/matita/tests/coercions_contravariant/c.con. +coercion cic:/matita/tests/coercions_contravariant/d.con. definition foo := λn,n1,m,m1.(λx.d m m1 (f n m (c n1 n x)) : A1 n1 -> B1 m1). definition foo1_1 := λn,n1,m,m1.(f n m : A1 n1 -> B1 m1). @@ -35,4 +35,4 @@ definition foo1_1 := λn,n1,m,m1.(f n m : A1 n1 -> B1 m1). definition h := λn,m.λx:A n.g m. definition foo2 := λn,n1,m,m1.(h n m : A1 n1 -> B1 m1). definition foo3 := λn1,n,m,m1.(h n m : A1 n1 -> B1 m1). -definition foo4 := λn1,n,m1,m.(h n m : A1 n1 -> B1 m1). \ No newline at end of file +definition foo4 := λn1,n,m1,m.(h n m : A1 n1 -> B1 m1). diff --git a/matita/tests/coercions_dependent.ma b/matita/tests/coercions_dependent.ma index b89abbf21..3b6602bbb 100644 --- a/matita/tests/coercions_dependent.ma +++ b/matita/tests/coercions_dependent.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/". + include "nat/nat.ma". include "list/list.ma". @@ -27,7 +27,7 @@ axiom c : ∀A,B.∀l:list A.vec B (length A l). axiom veclen : ∀A,n.vec A n -> nat. -coercion cic:/matita/test/c.con. +coercion cic:/matita/tests/coercions_dependent/c.con. alias num (instance 0) = "natural number". definition xxx := veclen nat ? [3; 4; 7]. diff --git a/matita/tests/coercions_dupelim.ma b/matita/tests/coercions_dupelim.ma index bfe2b3438..5c1c0c9f8 100644 --- a/matita/tests/coercions_dupelim.ma +++ b/matita/tests/coercions_dupelim.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/". + include "nat/nat.ma". diff --git a/matita/tests/coercions_nonuniform.ma b/matita/tests/coercions_nonuniform.ma index 0cf156537..f21d82911 100644 --- a/matita/tests/coercions_nonuniform.ma +++ b/matita/tests/coercions_nonuniform.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/coercions_nonuniform/". + axiom A : Type. axiom B : A -> Type. @@ -21,7 +21,7 @@ axiom f1 : A -> A. axiom k : ∀a:A.B (f a). -coercion cic:/matita/test/coercions_nonuniform/k.con. +coercion cic:/matita/tests/coercions_nonuniform/k.con. axiom C : Type. @@ -33,8 +33,8 @@ axiom C : Type. axiom c2 : ∀a.B (f a) -> B (f1 a). axiom c1 : ∀a:A. B (f1 a) -> C. -coercion cic:/matita/test/coercions_nonuniform/c1.con. -coercion cic:/matita/test/coercions_nonuniform/c2.con. +coercion cic:/matita/tests/coercions_nonuniform/c1.con. +coercion cic:/matita/tests/coercions_nonuniform/c2.con. axiom g : C -> C. @@ -43,4 +43,4 @@ definition test := λa:A.g a. (* Coq < Coercion c1 : B >-> C. User error: c1 does not respect the inheritance uniform condition -*) \ No newline at end of file +*) diff --git a/matita/tests/coercions_open.ma b/matita/tests/coercions_open.ma index d0d8caedb..69723aa89 100644 --- a/matita/tests/coercions_open.ma +++ b/matita/tests/coercions_open.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/". + include "logic/equality.ma". include "nat/nat.ma". @@ -27,12 +27,12 @@ axiom eatB : ∀n. B n -> A O. axiom jmcBA : ∀n,m.∀p:A n = B m.B m -> A n. axiom jmcAB : ∀n,m.∀p:A n = B m.A n -> B m. -coercion cic:/matita/test/jmcAB.con. -coercion cic:/matita/test/jmcBA.con. +coercion cic:/matita/tests/coercions_open/jmcAB.con. +coercion cic:/matita/tests/coercions_open/jmcBA.con. axiom daemon : ∀x,y:A O.x = y. alias num (instance 0) = "natural number". lemma xx : ∀b:B 2.∀a:A 1.eatA ? b = eatB ? a. intros; [3,5,7,9: apply AB|1: apply daemon];skip. -qed. \ No newline at end of file +qed. diff --git a/matita/tests/coercions_propagation.ma b/matita/tests/coercions_propagation.ma index 63c48e66b..7e3536b07 100644 --- a/matita/tests/coercions_propagation.ma +++ b/matita/tests/coercions_propagation.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/coercions_propagation/". + include "logic/connectives.ma". include "nat/orders.ma". @@ -21,15 +21,15 @@ inductive sigma (A:Type) (P:A → Prop) : Type ≝ sigma_intro: ∀a:A. P a → sigma A P. interpretation "sigma" 'exists \eta.x = - (cic:/matita/test/coercions_propagation/sigma.ind#xpointer(1/1) _ x). + (cic:/matita/tests/coercions_propagation/sigma.ind#xpointer(1/1) _ x). definition inject ≝ λP.λa:nat.λp:P a. sigma_intro ? P ? p. -coercion cic:/matita/test/coercions_propagation/inject.con 0 1. +coercion cic:/matita/tests/coercions_propagation/inject.con 0 1. definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ sigma_intro w _ ⇒ w]. -coercion cic:/matita/test/coercions_propagation/eject.con. +coercion cic:/matita/tests/coercions_propagation/eject.con. alias num (instance 0) = "natural number". theorem test: ∃n. 0 ≤ n. @@ -71,11 +71,11 @@ inductive NN (A:Type) : nat -> Type ≝ definition injectN ≝ λA,k.λP.λa:NN A k.λp:P a. sigma_intro ? P ? p. -coercion cic:/matita/test/coercions_propagation/injectN.con 0 1. +coercion cic:/matita/tests/coercions_propagation/injectN.con 0 1. definition ejectN ≝ λA,k.λP.λc: ∃n:NN A k.P n. match c with [ sigma_intro w _ ⇒ w]. -coercion cic:/matita/test/coercions_propagation/ejectN.con. +coercion cic:/matita/tests/coercions_propagation/ejectN.con. definition PN := λA,k.λx:NN A k. 1 <= k. diff --git a/matita/tests/coercions_russell.ma b/matita/tests/coercions_russell.ma index 36217ad9d..203faece5 100644 --- a/matita/tests/coercions_russell.ma +++ b/matita/tests/coercions_russell.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/russell/". + include "nat/orders.ma". include "list/list.ma". @@ -22,15 +22,15 @@ inductive sigma (A:Type) (P:A → Prop) : Type ≝ sig_intro: ∀a:A. P a → sigma A P. interpretation "sigma" 'exists \eta.x = - (cic:/matita/test/russell/sigma.ind#xpointer(1/1) _ x). + (cic:/matita/tests/coercions_russell/sigma.ind#xpointer(1/1) _ x). definition inject ≝ λP.λa:list nat.λp:P a. sig_intro ? P ? p. -coercion cic:/matita/test/russell/inject.con 0 1. +coercion cic:/matita/tests/coercions_russell/inject.con 0 1. definition eject ≝ λP.λc: ∃n:list nat.P n. match c with [ sig_intro w _ ⇒ w]. -coercion cic:/matita/test/russell/eject.con. +coercion cic:/matita/tests/coercions_russell/eject.con. alias symbol "exists" (instance 2) = "exists". lemma tl : ∀l:list nat. l ≠ [] → ∃l1.∃a.a :: l1 = l. @@ -55,7 +55,7 @@ qed. definition nat_return := λn:nat. Some ? n. -coercion cic:/matita/test/russell/nat_return.con. +coercion cic:/matita/tests/coercions_russell/nat_return.con. definition raise_exn := None nat. @@ -76,11 +76,11 @@ include "nat/compare.ma". definition inject_opt ≝ λP.λa:option nat.λp:P a. sig_intro ? P ? p. -coercion cic:/matita/test/russell/inject_opt.con 0 1. +coercion cic:/matita/tests/coercions_russell/inject_opt.con 0 1. definition eject_opt ≝ λP.λc: ∃n:option nat.P n. match c with [ sig_intro w _ ⇒ w]. -coercion cic:/matita/test/russell/eject_opt.con. +coercion cic:/matita/tests/coercions_russell/eject_opt.con. (* we may define mem as in the following lemma and get rid of it *) definition find_spec ≝ @@ -106,7 +106,7 @@ definition if : ∀A:Type.bool → A → A → A ≝ notation < "'If' \nbsp b \nbsp 'Then' \nbsp t \nbsp 'Else' \nbsp f" for @{ 'if $b $t $f }. notation > "'If' b 'Then' t 'Else' f" for @{ 'if $b $t $f }. -interpretation "if" 'if a b c = (cic:/matita/test/russell/if.con _ a b c). +interpretation "if" 'if a b c = (cic:/matita/tests/coercions_russell/if.con _ a b c). definition sigma_find_spec : ∀p,l. sigma ? (λres.find_spec l p res). (* define the find function *) diff --git a/matita/tests/comments.ma b/matita/tests/comments.ma index cb54a90d3..dfb631203 100644 --- a/matita/tests/comments.ma +++ b/matita/tests/comments.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/comments/". -include "../legacy/coq.ma". + +include "coq.ma". (* commento che va nell'ast, ma non viene contato come step perche' non e' un executable diff --git a/matita/tests/compose.ma b/matita/tests/compose.ma index 5d6035777..02316c6e0 100644 --- a/matita/tests/compose.ma +++ b/matita/tests/compose.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/compose/LCL002-1". + include "logic/equality.ma". theorem an_1: diff --git a/matita/tests/constructor.ma b/matita/tests/constructor.ma index f33044f12..8e785ba82 100644 --- a/matita/tests/constructor.ma +++ b/matita/tests/constructor.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/constructor". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/matita/tests/continuationals.ma b/matita/tests/continuationals.ma index a9d85ce25..ad9d73c4b 100644 --- a/matita/tests/continuationals.ma +++ b/matita/tests/continuationals.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/continuationals". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". diff --git a/matita/tests/contradiction.ma b/matita/tests/contradiction.ma index ed1ef6b3c..a8d8bc3b1 100644 --- a/matita/tests/contradiction.ma +++ b/matita/tests/contradiction.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/contradiction". -include "../legacy/coq.ma". + +include "coq.ma". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". alias id "not" = "cic:/Coq/Init/Logic/not.con". alias num (instance 0) = "natural number". diff --git a/matita/tests/cut.ma b/matita/tests/cut.ma index 24d17f13d..1de0ead4a 100644 --- a/matita/tests/cut.ma +++ b/matita/tests/cut.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/cut". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma index 40f8d3700..5308f9350 100644 --- a/matita/tests/decl.ma +++ b/matita/tests/decl.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/decl". + include "nat/times.ma". include "nat/orders.ma". diff --git a/matita/tests/decompose.ma b/matita/tests/decompose.ma index 2ba58c158..39d04755e 100644 --- a/matita/tests/decompose.ma +++ b/matita/tests/decompose.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/decompose". + include "logic/connectives.ma". diff --git a/matita/tests/demodulation_coq.ma b/matita/tests/demodulation_coq.ma index cb7a830eb..037f19260 100644 --- a/matita/tests/demodulation_coq.ma +++ b/matita/tests/demodulation_coq.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/demodulation/". -include "../legacy/coq.ma". + +include "coq.ma". alias num = "Coq natural number". alias symbol "times" = "Coq's natural times". diff --git a/matita/tests/demodulation_matita.ma b/matita/tests/demodulation_matita.ma index 0f4827e46..d1201a6c4 100644 --- a/matita/tests/demodulation_matita.ma +++ b/matita/tests/demodulation_matita.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/demodulation_matita/". + include "nat/minus.ma". diff --git a/matita/tests/dependent_injection.ma b/matita/tests/dependent_injection.ma index e217a7652..c58da98a9 100644 --- a/matita/tests/dependent_injection.ma +++ b/matita/tests/dependent_injection.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/dependent_injection". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)". diff --git a/matita/tests/dependent_type_inference.ma b/matita/tests/dependent_type_inference.ma index 11a42acac..d52faff17 100644 --- a/matita/tests/dependent_type_inference.ma +++ b/matita/tests/dependent_type_inference.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/dependent_type_inference/". + include "nat/nat.ma". diff --git a/matita/tests/destruct.ma b/matita/tests/destruct.ma index 55275c480..5a61101ca 100644 --- a/matita/tests/destruct.ma +++ b/matita/tests/destruct.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/discriminate". + include "logic/equality.ma". include "nat/nat.ma". diff --git a/matita/tests/elim.ma b/matita/tests/elim.ma index e038c5da2..42dc195cb 100644 --- a/matita/tests/elim.ma +++ b/matita/tests/elim.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/elim". -include "../legacy/coq.ma". + +include "coq.ma". inductive stupidtype: Set \def | Base : stupidtype diff --git a/matita/tests/fguidi.ma b/matita/tests/fguidi.ma index a95e954c1..b6bc3d907 100644 --- a/matita/tests/fguidi.ma +++ b/matita/tests/fguidi.ma @@ -12,13 +12,13 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/fguidi/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". -alias id "le" = "cic:/matita/fguidi/le.ind#xpointer(1/1)". +alias id "le" = "cic:/matita/tests/fguidi/le.ind#xpointer(1/1)". alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con". alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)". alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)". diff --git a/matita/tests/first.ma b/matita/tests/first.ma index 4fca7b199..bbd1e11c1 100644 --- a/matita/tests/first.ma +++ b/matita/tests/first.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/first/". + inductive nat : Set \def | O : nat diff --git a/matita/tests/fix_betareduction.ma b/matita/tests/fix_betareduction.ma index 65c916f17..cf85e58a8 100644 --- a/matita/tests/fix_betareduction.ma +++ b/matita/tests/fix_betareduction.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/fix_betareduction/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". alias id "n" = "cic:/Suresnes/BDD/canonicite/Canonicity_BDT/n.con". diff --git a/matita/tests/fold.ma b/matita/tests/fold.ma index cd507c7de..f21615185 100644 --- a/matita/tests/fold.ma +++ b/matita/tests/fold.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/fold". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/matita/tests/generalize.ma b/matita/tests/generalize.ma index a3aacd3bf..077eb3265 100644 --- a/matita/tests/generalize.ma +++ b/matita/tests/generalize.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/generalize". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "Coq natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/matita/tests/hard_refine.ma b/matita/tests/hard_refine.ma index 059a27be3..88adc389b 100644 --- a/matita/tests/hard_refine.ma +++ b/matita/tests/hard_refine.ma @@ -1,5 +1,5 @@ -set "baseuri" "cic:/matita/TPTP/BOO024-1". -include "../legacy/coq.ma". + +include "coq.ma". alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". (* Inclusion of: BOO024-1.p *) (* -------------------------------------------------------------------------- *) diff --git a/matita/tests/injection.ma b/matita/tests/injection.ma index 2cc7110ff..b805df687 100644 --- a/matita/tests/injection.ma +++ b/matita/tests/injection.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/injection". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)". diff --git a/matita/tests/interactive/automatic_insertion.ma b/matita/tests/interactive/automatic_insertion.ma index 56212bdc5..c2a5c2c54 100644 --- a/matita/tests/interactive/automatic_insertion.ma +++ b/matita/tests/interactive/automatic_insertion.ma @@ -12,6 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/xxx". + theorem t: And True (eq nat O O). split. exact (refl_equal nat O). exact I. qed. \ No newline at end of file diff --git a/matita/tests/interactive/drop.ma b/matita/tests/interactive/drop.ma index b8718cdb8..eefcd378b 100644 --- a/matita/tests/interactive/drop.ma +++ b/matita/tests/interactive/drop.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/drop". + alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias num (instance 0) = "natural number". diff --git a/matita/tests/interactive/grafite.ma b/matita/tests/interactive/grafite.ma index aaf570091..e71310a26 100644 --- a/matita/tests/interactive/grafite.ma +++ b/matita/tests/interactive/grafite.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/grafite/". + (* commento *) (** hint. *) diff --git a/matita/tests/interactive/test5.ma b/matita/tests/interactive/test5.ma index e48cc827e..8f36be288 100644 --- a/matita/tests/interactive/test5.ma +++ b/matita/tests/interactive/test5.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/interactive/test5/". + whelp instance \lambda A:Set. diff --git a/matita/tests/interactive/test6.ma b/matita/tests/interactive/test6.ma index 4afdd3741..42a99ff1b 100644 --- a/matita/tests/interactive/test6.ma +++ b/matita/tests/interactive/test6.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/interactive/test6/". + whelp instance \lambda A:Set. diff --git a/matita/tests/interactive/test7.ma b/matita/tests/interactive/test7.ma index d7347ed9f..55f22643a 100644 --- a/matita/tests/interactive/test7.ma +++ b/matita/tests/interactive/test7.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/interactive/test7/". + whelp instance \lambda A:Set. diff --git a/matita/tests/interactive/test_instance.ma b/matita/tests/interactive/test_instance.ma index 7e02c0fff..7aed7b6f8 100644 --- a/matita/tests/interactive/test_instance.ma +++ b/matita/tests/interactive/test_instance.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/tests/interactive/instance/". + whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x:A. P x x. whelp instance \lambda A:Set.\lambda P:A \to A \to Prop.\forall x,y:A. P x y \to P y x. diff --git a/matita/tests/inversion.ma b/matita/tests/inversion.ma index 4c33beee0..f99acff11 100644 --- a/matita/tests/inversion.ma +++ b/matita/tests/inversion.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/inversion_sum/". -include "../legacy/coq.ma". + +include "coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/matita/tests/inversion2.ma b/matita/tests/inversion2.ma index c99c59bcf..8261b33f0 100644 --- a/matita/tests/inversion2.ma +++ b/matita/tests/inversion2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/inversion2/". -include "../legacy/coq.ma". + +include "coq.ma". inductive nat : Set \def O : nat diff --git a/matita/tests/letrec.ma b/matita/tests/letrec.ma index 55933cd31..734a4a962 100644 --- a/matita/tests/letrec.ma +++ b/matita/tests/letrec.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/letrec/". + alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". diff --git a/matita/tests/letrecand.ma b/matita/tests/letrecand.ma index d9dfec329..d2ac486b4 100644 --- a/matita/tests/letrecand.ma +++ b/matita/tests/letrecand.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/letrecand". + include "nat/nat.ma". diff --git a/matita/tests/match_inference.ma b/matita/tests/match_inference.ma index 0e27ce409..539fac9cc 100644 --- a/matita/tests/match_inference.ma +++ b/matita/tests/match_inference.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/match_inference/". + inductive pos: Set \def | one : pos diff --git a/matita/tests/metasenv_ordering.ma b/matita/tests/metasenv_ordering.ma index de9746d52..ff61c9da6 100644 --- a/matita/tests/metasenv_ordering.ma +++ b/matita/tests/metasenv_ordering.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/metasenv_ordering". -include "../legacy/coq.ma". + +include "coq.ma". alias num (instance 0) = "natural number". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". diff --git a/matita/tests/multiple_inheritance.ma b/matita/tests/multiple_inheritance.ma index df15e704f..1aa708fb1 100644 --- a/matita/tests/multiple_inheritance.ma +++ b/matita/tests/multiple_inheritance.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/". + include "logic/equality.ma". @@ -31,7 +31,7 @@ lemma r2 : R → R2. [ exact (C r) | rewrite > (with_ r); exact (mult (r2_ r))] qed. -coercion cic:/matita/test/r2.con. +coercion cic:/matita/tests/multiple_inheritance/r2.con. (* convertibility test *) lemma conv_test : ∀r:R.C r -> K r. diff --git a/matita/tests/mysql_escaping.ma b/matita/tests/mysql_escaping.ma index bd0eb8d5a..e9e6c8b1b 100644 --- a/matita/tests/mysql_escaping.ma +++ b/matita/tests/mysql_escaping.ma @@ -12,6 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/mysql_escaping/". + theorem a' : Prop \to Prop.intros.assumption.qed. diff --git a/matita/tests/naiveparamod.ma b/matita/tests/naiveparamod.ma index 624604842..ef86f372d 100644 --- a/matita/tests/naiveparamod.ma +++ b/matita/tests/naiveparamod.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/naiveparamod". + include "logic/equality.ma". diff --git a/matita/tests/overred.ma b/matita/tests/overred.ma index 2034001bd..b270912ad 100644 --- a/matita/tests/overred.ma +++ b/matita/tests/overred.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/overred/". + include "logic/equality.ma". @@ -24,10 +24,10 @@ definition T3 : Type := T2. axiom t3 : T3. axiom c : T2 -> X -> X. -coercion cic:/matita/test/overred/c.con 1. +coercion cic:/matita/tests/overred/c.con 1. axiom daemon : c t3 x = x. theorem find_a_coercion_from_T2_for_a_term_in_T3 : (* c *) t3 x = x. apply daemon. -qed. \ No newline at end of file +qed. diff --git a/matita/tests/paramodulation.ma b/matita/tests/paramodulation.ma index 2d090e1b0..074dcc96a 100644 --- a/matita/tests/paramodulation.ma +++ b/matita/tests/paramodulation.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/paramodulation". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias symbol "plus" (instance 0) = "Coq's natural plus". diff --git a/matita/tests/paramodulation/BOO075-1.ma b/matita/tests/paramodulation/BOO075-1.ma index 7c46167f4..67a89bf6c 100644 --- a/matita/tests/paramodulation/BOO075-1.ma +++ b/matita/tests/paramodulation/BOO075-1.ma @@ -1,4 +1,4 @@ -set "baseuri" "cic:/matita/TPTP/BOO075-1". + inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x. @@ -30,17 +30,17 @@ intros.elim H1.assumption. qed. default "equality" - cic:/matita/TPTP/BOO075-1/eq.ind - cic:/matita/TPTP/BOO075-1/sym_eq.con - cic:/matita/TPTP/BOO075-1/trans_eq.con - cic:/matita/TPTP/BOO075-1/eq_ind.con - cic:/matita/TPTP/BOO075-1/eq_elim_r.con - cic:/matita/TPTP/BOO075-1/eq_rec.con - cic:/matita/TPTP/BOO075-1/eq_elim_r'.con - cic:/matita/TPTP/BOO075-1/eq_rect.con - cic:/matita/TPTP/BOO075-1/eq_elim_r''.con - cic:/matita/TPTP/BOO075-1/eq_f.con - cic:/matita/TPTP/BOO075-1/eq_f1.con. + cic:/matita/tests/paramodulation/BOO075-1/eq.ind + cic:/matita/tests/paramodulation/BOO075-1/sym_eq.con + cic:/matita/tests/paramodulation/BOO075-1/trans_eq.con + cic:/matita/tests/paramodulation/BOO075-1/eq_ind.con + cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r.con + cic:/matita/tests/paramodulation/BOO075-1/eq_rec.con + cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r'.con + cic:/matita/tests/paramodulation/BOO075-1/eq_rect.con + cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r''.con + cic:/matita/tests/paramodulation/BOO075-1/eq_f.con + cic:/matita/tests/paramodulation/BOO075-1/eq_f1.con. theorem eq_f: \forall A,B:Type.\forall f:A\to B. \forall x,y:A. eq A x y \to eq B (f x) (f y). @@ -55,7 +55,7 @@ qed. inductive ex (A:Type) (P:A \to Prop) : Prop \def ex_intro: \forall x:A. P x \to ex A P. interpretation "exists" 'exists \eta.x = - (cic:/matita/TPTP/BOO075-1/ex.ind#xpointer(1/1) _ x). + (cic:/matita/tests/paramodulation/BOO075-1/ex.ind#xpointer(1/1) _ x). notation < "hvbox(\exists ident i opt (: ty) break . p)" right associative with precedence 20 diff --git a/matita/tests/paramodulation/boolean_algebra.ma b/matita/tests/paramodulation/boolean_algebra.ma index ab47854da..6822cfb3e 100644 --- a/matita/tests/paramodulation/boolean_algebra.ma +++ b/matita/tests/paramodulation/boolean_algebra.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/SK/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". diff --git a/matita/tests/paramodulation/group.ma b/matita/tests/paramodulation/group.ma index 621e2d449..c8645cc82 100644 --- a/matita/tests/paramodulation/group.ma +++ b/matita/tests/paramodulation/group.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/paramodulation/group". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". diff --git a/matita/tests/paramodulation/irratsqrt2.ma b/matita/tests/paramodulation/irratsqrt2.ma index 5c976bcb9..5f845b4f0 100644 --- a/matita/tests/paramodulation/irratsqrt2.ma +++ b/matita/tests/paramodulation/irratsqrt2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/paramodulation/irratsqrt2/". + include "nat/times.ma". include "nat/minus.ma". diff --git a/matita/tests/pullback.ma b/matita/tests/pullback.ma index 935a90dcf..1196255d9 100644 --- a/matita/tests/pullback.ma +++ b/matita/tests/pullback.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/pullback". + inductive T : Type \def t : T. inductive L : Type \def l : L. diff --git a/matita/tests/record.ma b/matita/tests/record.ma index bc5d2e217..24bed8ade 100644 --- a/matita/tests/record.ma +++ b/matita/tests/record.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/record/". + record empty : Type \def {}. diff --git a/matita/tests/replace.ma b/matita/tests/replace.ma index 2961fdc7e..37a530978 100644 --- a/matita/tests/replace.ma +++ b/matita/tests/replace.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/replace/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "Coq natural number". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". diff --git a/matita/tests/rewrite.ma b/matita/tests/rewrite.ma index dff3b2300..a1956c9b5 100644 --- a/matita/tests/rewrite.ma +++ b/matita/tests/rewrite.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/rewrite/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias num (instance 0) = "Coq natural number". diff --git a/matita/tests/second.ma b/matita/tests/second.ma index 450c67671..284be0701 100644 --- a/matita/tests/second.ma +++ b/matita/tests/second.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/second/". + alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)". alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)". alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)". diff --git a/matita/tests/simpl.ma b/matita/tests/simpl.ma index 61150e817..7af3f5521 100644 --- a/matita/tests/simpl.ma +++ b/matita/tests/simpl.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/simpl/". -include "../legacy/coq.ma". + +include "coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". alias id "plus" = "cic:/Coq/Init/Peano/plus.con". diff --git a/matita/tests/tacticals.ma b/matita/tests/tacticals.ma index a44e80a86..f1e8998f0 100644 --- a/matita/tests/tacticals.ma +++ b/matita/tests/tacticals.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/test/tacticals". + inductive myand (A, B: Prop) : Prop \def | myconj : ∀a:A.∀b:B. myand A B. diff --git a/matita/tests/test2.ma b/matita/tests/test2.ma index 93da2ecce..bcd2def53 100644 --- a/matita/tests/test2.ma +++ b/matita/tests/test2.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/test2/". -include "../legacy/coq.ma". + +include "coq.ma". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias symbol "and" (instance 0) = "Coq's logical and". diff --git a/matita/tests/test3.ma b/matita/tests/test3.ma index 85180da5b..a2e2e40df 100644 --- a/matita/tests/test3.ma +++ b/matita/tests/test3.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/test3/". -include "../legacy/coq.ma". + +include "coq.ma". alias symbol "eq" (instance 0) = "Coq's leibnitz's equality". theorem a:\forall x.x=x. diff --git a/matita/tests/test4.ma b/matita/tests/test4.ma index 55cfb6aaf..a8e219fcb 100644 --- a/matita/tests/test4.ma +++ b/matita/tests/test4.ma @@ -12,8 +12,8 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/test4/". -include "../legacy/coq.ma". + +include "coq.ma". (* commento che va nell'ast, ma non viene contato diff --git a/matita/tests/third.ma b/matita/tests/third.ma index 124cdc121..70041dc3a 100644 --- a/matita/tests/third.ma +++ b/matita/tests/third.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/third/". + alias id "nat" = "cic:/matita/tests/first/nat.ind#xpointer(1/1)". alias id "O" = "cic:/matita/tests/first/nat.ind#xpointer(1/1/1)". alias id "eq" = "cic:/matita/tests/first/eq.ind#xpointer(1/1)". diff --git a/matita/tests/tinycals.ma b/matita/tests/tinycals.ma index 465d7c06e..3ceba6eaa 100644 --- a/matita/tests/tinycals.ma +++ b/matita/tests/tinycals.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/tests/tinycals". + theorem prova: \forall A,B,C:Prop. diff --git a/matita/tests/unfold.ma b/matita/tests/unfold.ma index 3318db17d..a4bd93150 100644 --- a/matita/tests/unfold.ma +++ b/matita/tests/unfold.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/unfold". -include "../legacy/coq.ma". + +include "coq.ma". alias symbol "plus" (instance 0) = "Coq's natural plus". definition myplus \def \lambda x,y. x+y. -- 2.39.2