X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Ftests%2Fdepends;h=ccbafd0cdb51de3a32f94b18e408b0a402543405;hb=b97a7976503b2d2e5cbc9199f848135a324775a8;hp=77c709c7004ed9d4fc7ff7d4125cb51475fca645;hpb=42f25c258b0b199ee96dd8eaa3d44c86eb6916ab;p=helm.git diff --git a/helm/software/matita/tests/depends b/helm/software/matita/tests/depends index 77c709c70..ccbafd0cd 100644 --- a/helm/software/matita/tests/depends +++ b/helm/software/matita/tests/depends @@ -1,5 +1,5 @@ -TPTP/Veloci/GRP570-1.p.ma logic/equality.ma TPTP/Veloci/GRP595-1.p.ma logic/equality.ma +TPTP/Veloci/GRP570-1.p.ma logic/equality.ma dependent_guarded_bove_capretta.ma nat/nat.ma interactive/test5.ma TPTP/Veloci/SYN083-1.p.ma logic/equality.ma @@ -35,8 +35,8 @@ TPTP/Veloci/COL063-3.p.ma logic/equality.ma TPTP/Veloci/LCL112-2.p.ma logic/equality.ma formal_topology.ma logic/connectives.ma TPTP/Veloci/RNG023-7.p.ma logic/equality.ma -replace.ma coq.ma test2.ma coq.ma +replace.ma coq.ma TPTP/Veloci/COL064-7.p.ma logic/equality.ma TPTP/Veloci/BOO009-2.p.ma logic/equality.ma TPTP/Veloci/GRP510-1.p.ma logic/equality.ma @@ -78,6 +78,7 @@ TPTP/Veloci/BOO006-4.p.ma logic/equality.ma TPTP/Veloci/BOO003-2.p.ma logic/equality.ma TPTP/Veloci/RNG024-6.p.ma logic/equality.ma bool.ma coq.ma +ng_tactics.ma logic/connectives.ma nat/plus.ma ng_pts.ma TPTP/Veloci/BOO011-2.p.ma logic/equality.ma TPTP/Veloci/LCL154-1.p.ma logic/equality.ma TPTP/Veloci/LCL114-2.p.ma logic/equality.ma @@ -85,23 +86,23 @@ letrec.ma TPTP/Veloci/BOO001-1.p.ma logic/equality.ma TPTP/Veloci/GRP160-1.p.ma logic/equality.ma TPTP/Veloci/GRP600-1.p.ma logic/equality.ma -TPTP/Veloci/COL063-5.p.ma logic/equality.ma TPTP/Veloci/GRP512-1.p.ma logic/equality.ma +TPTP/Veloci/COL063-5.p.ma logic/equality.ma continuationals.ma coq.ma TPTP/Veloci/GRP490-1.p.ma logic/equality.ma TPTP/Veloci/BOO034-1.p.ma logic/equality.ma fold.ma coq.ma +ng_pts.ma TPTP/Veloci/GRP545-1.p.ma logic/equality.ma TPTP/Veloci/GRP520-1.p.ma logic/equality.ma -a.ma TPTP/Veloci/GRP457-1.p.ma logic/equality.ma TPTP/Veloci/COL064-9.p.ma logic/equality.ma TPTP/Veloci/BOO009-4.p.ma logic/equality.ma TPTP/Veloci/LAT040-1.p.ma logic/equality.ma TPTP/Veloci/GRP578-1.p.ma logic/equality.ma change.ma coq.ma -TPTP/Veloci/GRP168-1.p.ma logic/equality.ma TPTP/Veloci/BOO075-1.p.ma logic/equality.ma +TPTP/Veloci/GRP168-1.p.ma logic/equality.ma TPTP/Veloci/GRP143-1.p.ma logic/equality.ma TPTP/Veloci/GRP586-1.p.ma logic/equality.ma TPTP/Veloci/GRP561-1.p.ma logic/equality.ma @@ -117,8 +118,8 @@ TPTP/Veloci/RNG007-4.p.ma logic/equality.ma TPTP/Veloci/GRP548-1.p.ma logic/equality.ma TPTP/Veloci/GRP182-3.p.ma logic/equality.ma TPTP/Veloci/COL048-1.p.ma logic/equality.ma -TPTP/Veloci/BOO005-2.p.ma logic/equality.ma TPTP/Veloci/GRP189-2.p.ma logic/equality.ma +TPTP/Veloci/BOO005-2.p.ma logic/equality.ma TPTP/Veloci/GRP556-1.p.ma logic/equality.ma TPTP/Veloci/GRP146-1.p.ma logic/equality.ma TPTP/Veloci/COL064-4.p.ma logic/equality.ma @@ -130,6 +131,7 @@ TPTP/Veloci/GRP154-1.p.ma logic/equality.ma TPTP/Veloci/ROB009-1.p.ma logic/equality.ma TPTP/Veloci/LCL164-1.p.ma logic/equality.ma TPTP/Veloci/BOO003-4.p.ma logic/equality.ma +ng_elim.ma ng_pts.ma TPTP/Veloci/GRP597-1.p.ma logic/equality.ma TPTP/Veloci/GRP572-1.p.ma logic/equality.ma TPTP/Veloci/GRP484-1.p.ma logic/equality.ma @@ -140,8 +142,8 @@ TPTP/Veloci/GRP580-1.p.ma logic/equality.ma TPTP/Veloci/COL062-3.p.ma logic/equality.ma TPTP/Veloci/GRP492-1.p.ma logic/equality.ma cut.ma coq.ma -TPTP/Veloci/LAT034-1.p.ma logic/equality.ma TPTP/Veloci/COL018-1.p.ma logic/equality.ma +TPTP/Veloci/LAT034-1.p.ma logic/equality.ma tinycals.ma logic/connectives.ma coercions_contravariant.ma logic/equality.ma nat/nat.ma interactive/automatic_insertion.ma @@ -149,22 +151,24 @@ clearbody.ma coq.ma TPTP/Veloci/LCL134-1.p.ma logic/equality.ma TPTP/Veloci/COL060-2.p.ma logic/equality.ma TPTP/Veloci/BOO016-2.p.ma logic/equality.ma -TPTP/Veloci/LAT039-2.p.ma logic/equality.ma TPTP/Veloci/GRP542-1.p.ma logic/equality.ma +TPTP/Veloci/LAT039-2.p.ma logic/equality.ma +TPTP/Veloci/GRP157-1.p.ma logic/equality.ma TPTP/Veloci/GRP186-4.p.ma logic/equality.ma TPTP/Veloci/GRP454-1.p.ma logic/equality.ma -TPTP/Veloci/GRP157-1.p.ma logic/equality.ma TPTP/Veloci/GRP509-1.p.ma logic/equality.ma TPTP/Veloci/GRP550-1.p.ma logic/equality.ma +ng_commands.ma nat/nat.ma ng_pts.ma TPTP/Veloci/GRP487-1.p.ma logic/equality.ma +paratest.ma nat/plus.ma paramodulation/BOO075-1.ma TPTP/Veloci/GRP605-1.p.ma logic/equality.ma fguidi.ma logic/connectives.ma nat/nat.ma TPTP/Veloci/GRP583-1.p.ma logic/equality.ma TPTP/Veloci/GRP517-1.p.ma logic/equality.ma -TPTP/Veloci/GRP173-1.p.ma logic/equality.ma -TPTP/Veloci/GRP495-1.p.ma logic/equality.ma TPTP/Veloci/COL083-1.p.ma logic/equality.ma +TPTP/Veloci/GRP495-1.p.ma logic/equality.ma +TPTP/Veloci/GRP173-1.p.ma logic/equality.ma coercions_propagation.ma logic/connectives.ma nat/orders.ma TPTP/Veloci/LAT045-1.p.ma logic/equality.ma TPTP/Veloci/GRP558-1.p.ma logic/equality.ma @@ -188,8 +192,8 @@ TPTP/Veloci/LCL153-1.p.ma logic/equality.ma pullback.ma logic/equality.ma TPTP/Veloci/COL086-1.p.ma logic/equality.ma TPTP/Veloci/GRP151-1.p.ma logic/equality.ma -TPTP/Veloci/GRP616-1.p.ma logic/equality.ma TPTP/Veloci/LCL161-1.p.ma logic/equality.ma +TPTP/Veloci/GRP616-1.p.ma logic/equality.ma TPTP/Veloci/GRP023-2.p.ma logic/equality.ma TPTP/Veloci/GRP206-1.p.ma logic/equality.ma decompose.ma logic/connectives.ma @@ -204,8 +208,8 @@ dependent_type_inference.ma nat/nat.ma TPTP/Veloci/GRP456-1.p.ma logic/equality.ma TPTP/Veloci/GRP159-1.p.ma logic/equality.ma TPTP/Veloci/ROB030-1.p.ma logic/equality.ma -TPTP/Veloci/GRP552-1.p.ma logic/equality.ma TPTP/Veloci/GRP577-1.p.ma logic/equality.ma +TPTP/Veloci/GRP552-1.p.ma logic/equality.ma TPTP/Veloci/BOO013-2.p.ma logic/equality.ma rewrite.ma coq.ma bad_tests/auto.ma coq.ma @@ -218,16 +222,16 @@ TPTP/Veloci/GRP602-1.p.ma logic/equality.ma TPTP/Veloci/GRP514-1.p.ma logic/equality.ma TPTP/Veloci/LCL139-1.p.ma logic/equality.ma TPTP/Veloci/GRP547-1.p.ma logic/equality.ma -TPTP/Veloci/GRP137-1.p.ma logic/equality.ma +TPTP/Veloci/COL004-3.p.ma logic/equality.ma TPTP/Veloci/GRP459-1.p.ma logic/equality.ma TPTP/Veloci/BOO069-1.p.ma logic/equality.ma -TPTP/Veloci/COL004-3.p.ma logic/equality.ma +TPTP/Veloci/GRP137-1.p.ma logic/equality.ma TPTP/Veloci/GRP188-2.p.ma logic/equality.ma apply.ma coq.ma TPTP/Veloci/GRP467-1.p.ma logic/equality.ma TPTP/Veloci/GRP145-1.p.ma logic/equality.ma -TPTP/Veloci/LCL155-1.p.ma logic/equality.ma TPTP/Veloci/COL063-4.p.ma logic/equality.ma +TPTP/Veloci/LCL155-1.p.ma logic/equality.ma TPTP/Veloci/GRP588-1.p.ma logic/equality.ma TPTP/Veloci/GRP153-1.p.ma logic/equality.ma paramodulation.ma coq.ma @@ -236,8 +240,8 @@ coercions_nonuniform.ma TPTP/Veloci/GRP161-1.p.ma logic/equality.ma TPTP/Veloci/COL064-8.p.ma logic/equality.ma TPTP/Veloci/LDA001-1.p.ma logic/equality.ma -TPTP/Veloci/COL050-1.p.ma logic/equality.ma TPTP/Veloci/BOO010-4.p.ma logic/equality.ma +TPTP/Veloci/COL050-1.p.ma logic/equality.ma TPTP/Veloci/LCL110-2.p.ma logic/equality.ma TPTP/Veloci/GRP491-1.p.ma logic/equality.ma TPTP/Veloci/COL061-3.p.ma logic/equality.ma @@ -246,9 +250,9 @@ TPTP/Veloci/GRP613-1.p.ma logic/equality.ma compose.ma logic/equality.ma TPTP/Veloci/COL025-1.p.ma logic/equality.ma TPTP/Veloci/GRP115-1.p.ma logic/equality.ma +letrecand.ma nat/nat.ma unifhint.ma list/list.ma nat/nat.ma nat/plus.ma hard_refine.ma coq.ma -letrecand.ma nat/nat.ma paramodulation/group.ma coq.ma TPTP/Veloci/LCL158-1.p.ma logic/equality.ma TPTP/Veloci/LCL133-1.p.ma logic/equality.ma @@ -256,7 +260,6 @@ TPTP/Veloci/GRP566-1.p.ma logic/equality.ma TPTP/Veloci/GRP541-1.p.ma logic/equality.ma decl.ma nat/orders.ma nat/times.ma TPTP/Veloci/GRP156-1.p.ma logic/equality.ma -universe_inconsistency.ma mysql_escaping.ma TPTP/Veloci/LCL141-1.p.ma logic/equality.ma TPTP/Veloci/GRP182-2.p.ma logic/equality.ma @@ -266,8 +269,8 @@ TPTP/Veloci/GRP599-1.p.ma logic/equality.ma TPTP/Veloci/GRP574-1.p.ma logic/equality.ma TPTP/Veloci/LDA007-3.p.ma logic/equality.ma unfold.ma coq.ma -TPTP/Veloci/GRP189-1.p.ma logic/equality.ma TPTP/Veloci/GRP486-1.p.ma logic/equality.ma +TPTP/Veloci/GRP189-1.p.ma logic/equality.ma TPTP/Veloci/BOO071-1.p.ma logic/equality.ma TPTP/Veloci/BOO013-4.p.ma logic/equality.ma TPTP/Veloci/GRP582-1.p.ma logic/equality.ma @@ -287,8 +290,8 @@ injection.ma coq.ma second.ma first.ma TPTP/Veloci/COL062-2.p.ma logic/equality.ma match_inference.ma -unifhint_simple.ma logic/equality.ma simpl.ma coq.ma +unifhint_simple.ma logic/equality.ma TPTP/Veloci/COL063-6.p.ma logic/equality.ma TPTP/Veloci/GRP142-1.p.ma logic/equality.ma third.ma first.ma second.ma @@ -333,6 +336,7 @@ TPTP/Veloci/GRP136-1.p.ma logic/equality.ma TPTP/Veloci/GRP458-1.p.ma logic/equality.ma coercions_open.ma logic/equality.ma nat/nat.ma paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma +ng_uris_and_notation.ma nat/nat.ma ng_pts.ma TPTP/Veloci/GRP144-1.p.ma logic/equality.ma TPTP/Veloci/BOO018-4.p.ma logic/equality.ma TPTP/Veloci/LAT008-1.p.ma logic/equality.ma