From 8080b59026efcb6461512e5122fe94c03849d06d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 7 Jan 2008 15:01:06 +0000 Subject: [PATCH] added makefiles to allow make all/opt/clean/clean.opt --- matita/dama/Makefile | 10 ++ matita/dama/depends | 40 +++++ matita/dama/makefile | 33 ---- matita/dama/root | 1 + matita/legacy/Makefile | 10 ++ matita/legacy/depends | 1 + matita/legacy/root | 1 + matita/library/Makefile | 10 ++ matita/tests/Makefile | 10 ++ matita/tests/depends | 347 ++++++++++++++++++++++++++++++++++++++++ matita/tests/makefile | 37 ----- matita/tests/root | 2 + 12 files changed, 432 insertions(+), 70 deletions(-) create mode 100644 matita/dama/Makefile create mode 100644 matita/dama/depends delete mode 100644 matita/dama/makefile create mode 100644 matita/dama/root create mode 100644 matita/legacy/Makefile create mode 100644 matita/legacy/depends create mode 100644 matita/legacy/root create mode 100644 matita/library/Makefile create mode 100644 matita/tests/Makefile create mode 100644 matita/tests/depends delete mode 100644 matita/tests/makefile create mode 100644 matita/tests/root diff --git a/matita/dama/Makefile b/matita/dama/Makefile new file mode 100644 index 000000000..2eefa0cbd --- /dev/null +++ b/matita/dama/Makefile @@ -0,0 +1,10 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../matitac +$(DIR).opt opt all.opt: + ../matitac.opt +clean: + ../matitaclean +clean.opt: + ../matitaclean.opt diff --git a/matita/dama/depends b/matita/dama/depends new file mode 100644 index 000000000..a047fc9d1 --- /dev/null +++ b/matita/dama/depends @@ -0,0 +1,40 @@ +metric_lattice.ma lattice.ma metric_space.ma +metric_space.ma ordered_divisible_group.ma +sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma sequence.ma +premetric_lattice.ma lattice.ma metric_space.ma +ordered_group.ma group.ma +divisible_group.ma group.ma nat/orders.ma +ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma +sequence.ma excess.ma nat/orders.ma ordered_group.ma +constructive_connectives.ma logic/connectives.ma +group.ma excess.ma +prevalued_lattice.ma ordered_group.ma +excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma +Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma +lattice.ma excess.ma +constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma +constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma +classical_pointwise/topology.ma classical_pointwise/sets.ma +classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma +classical_pointwise/sets.ma logic/connectives.ma nat/nat.ma +classical_pointfree/ordered_sets.ma excess.ma +classical_pointfree/ordered_sets2.ma classical_pointfree/ordered_sets.ma +attic/fields.ma attic/rings.ma +attic/reals.ma attic/ordered_fields_ch0.ma +attic/integration_algebras.ma attic/vector_spaces.ma lattice.ma +attic/vector_spaces.ma attic/reals.ma +attic/rings.ma group.ma +attic/ordered_fields_ch0.ma group.ma attic/fields.ma ordered_group.ma +nat/nat.ma +logic/connectives.ma +higher_order_defs/relations.ma +Q/q.ma +nat/plus.ma +higher_order_defs/relations.ma +logic/connectives.ma +nat/orders.ma +nat/times.ma +nat/orders.ma +nat/orders.ma +nat/plus.ma +nat/orders.ma diff --git a/matita/dama/makefile b/matita/dama/makefile deleted file mode 100644 index ce86d1360..000000000 --- a/matita/dama/makefile +++ /dev/null @@ -1,33 +0,0 @@ -H=@ - -RT_BASEDIR=../ -OPTIONS=-bench -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -all: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) - -preall: - $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - diff --git a/matita/dama/root b/matita/dama/root new file mode 100644 index 000000000..c57405b94 --- /dev/null +++ b/matita/dama/root @@ -0,0 +1 @@ +baseuri=cic:/matita/ diff --git a/matita/legacy/Makefile b/matita/legacy/Makefile new file mode 100644 index 000000000..2eefa0cbd --- /dev/null +++ b/matita/legacy/Makefile @@ -0,0 +1,10 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../matitac +$(DIR).opt opt all.opt: + ../matitac.opt +clean: + ../matitaclean +clean.opt: + ../matitaclean.opt diff --git a/matita/legacy/depends b/matita/legacy/depends new file mode 100644 index 000000000..c35efdda5 --- /dev/null +++ b/matita/legacy/depends @@ -0,0 +1 @@ +coq.ma diff --git a/matita/legacy/root b/matita/legacy/root new file mode 100644 index 000000000..302ea9e6e --- /dev/null +++ b/matita/legacy/root @@ -0,0 +1 @@ +baseuri=cic:/matita/legacy diff --git a/matita/library/Makefile b/matita/library/Makefile new file mode 100644 index 000000000..2eefa0cbd --- /dev/null +++ b/matita/library/Makefile @@ -0,0 +1,10 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../matitac +$(DIR).opt opt all.opt: + ../matitac.opt +clean: + ../matitaclean +clean.opt: + ../matitaclean.opt diff --git a/matita/tests/Makefile b/matita/tests/Makefile new file mode 100644 index 000000000..2b1270eaa --- /dev/null +++ b/matita/tests/Makefile @@ -0,0 +1,10 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../matitac 2>/dev/null +$(DIR).opt opt all.opt: + ../matitac.opt 2>/dev/null +clean: + ../matitaclean +clean.opt: + ../matitaclean.opt diff --git a/matita/tests/depends b/matita/tests/depends new file mode 100644 index 000000000..9ae9703ec --- /dev/null +++ b/matita/tests/depends @@ -0,0 +1,347 @@ +naiveparamod.ma logic/equality.ma +coercions_nonuniform.ma +paramodulation.ma coq.ma +demodulation_coq.ma coq.ma +assumption.ma coq.ma +elim.ma coq.ma +generalize.ma coq.ma +comments.ma coq.ma +overred.ma logic/equality.ma +clear.ma coq.ma +metasenv_ordering.ma coq.ma +tinycals.ma logic/connectives.ma +demodulation_matita.ma nat/minus.ma +fguidi.ma coq.ma +inversion2.ma coq.ma +absurd.ma coq.ma +decompose.ma logic/connectives.ma +unfold.ma coq.ma +dependent_injection.ma coq.ma +tacticals.ma +multiple_inheritance.ma logic/equality.ma +second.ma first.ma +destruct.ma datatypes/constructors.ma logic/equality.ma nat/nat.ma +test3.ma coq.ma +continuationals.ma coq.ma +coercions_dupelim.ma logic/equality.ma nat/nat.ma +apply.ma coq.ma +coercions_open.ma logic/equality.ma nat/nat.ma +match_inference.ma +hard_refine.ma coq.ma +fix_betareduction.ma coq.ma +decl.ma nat/orders.ma nat/times.ma +pullback.ma +mysql_escaping.ma +rewrite.ma coq.ma +injection.ma coq.ma +contradiction.ma coq.ma +fold.ma coq.ma +coercions.ma nat/compare.ma nat/times.ma +record.ma +bad_induction.ma logic/equality.ma nat/nat.ma +first.ma +cut.ma coq.ma +letrecand.ma nat/nat.ma +coercions_contravariant.ma logic/equality.ma nat/nat.ma +test4.ma coq.ma +dependent_type_inference.ma nat/nat.ma +coercions_propagation.ma logic/connectives.ma nat/orders.ma +letrec.ma +apply2.ma nat/nat.ma +inversion.ma coq.ma +replace.ma coq.ma +applys.ma nat/div_and_mod.ma nat/factorial.ma nat/primes.ma +third.ma first.ma second.ma +simpl.ma coq.ma +coercions_dependent.ma decidable_kit/list_aux.ma list/list.ma nat/nat.ma +constructor.ma coq.ma +test2.ma coq.ma +compose.ma logic/equality.ma +coercions_russell.ma datatypes/bool.ma datatypes/constructors.ma list/list.ma list/sort.ma nat/compare.ma nat/orders.ma +clearbody.ma coq.ma +bool.ma coq.ma +change.ma coq.ma +interactive/grafite.ma +interactive/drop.ma +interactive/test7.ma +interactive/automatic_insertion.ma +interactive/test5.ma +interactive/test_instance.ma +interactive/test6.ma +bad_tests/baseuri.ma +bad_tests/auto.ma coq.ma +paramodulation/irratsqrt2.ma nat/minus.ma nat/times.ma +paramodulation/boolean_algebra.ma coq.ma +paramodulation/group.ma coq.ma +paramodulation/BOO075-1.ma +TPTP/Veloci/BOO012-4.p.ma logic/equality.ma +TPTP/Veloci/COL064-2.p.ma logic/equality.ma +TPTP/Veloci/COL012-1.p.ma logic/equality.ma +TPTP/Veloci/GRP570-1.p.ma logic/equality.ma +TPTP/Veloci/GRP189-1.p.ma logic/equality.ma +TPTP/Veloci/COL008-1.p.ma logic/equality.ma +TPTP/Veloci/COL062-3.p.ma logic/equality.ma +TPTP/Veloci/SYN083-1.p.ma logic/equality.ma +TPTP/Veloci/LAT039-2.p.ma logic/equality.ma +TPTP/Veloci/GRP173-1.p.ma logic/equality.ma +TPTP/Veloci/COL015-1.p.ma logic/equality.ma +TPTP/Veloci/RNG024-6.p.ma logic/equality.ma +TPTP/Veloci/COL062-2.p.ma logic/equality.ma +TPTP/Veloci/GRP576-1.p.ma logic/equality.ma +TPTP/Veloci/GRP137-1.p.ma logic/equality.ma +TPTP/Veloci/COL063-5.p.ma logic/equality.ma +TPTP/Veloci/COL045-1.p.ma logic/equality.ma +TPTP/Veloci/GRP011-4.p.ma logic/equality.ma +TPTP/Veloci/GRP578-1.p.ma logic/equality.ma +TPTP/Veloci/GRP168-1.p.ma logic/equality.ma +TPTP/Veloci/GRP588-1.p.ma logic/equality.ma +TPTP/Veloci/BOO005-2.p.ma logic/equality.ma +TPTP/Veloci/GRP161-1.p.ma logic/equality.ma +TPTP/Veloci/COL050-1.p.ma logic/equality.ma +TPTP/Veloci/GRP552-1.p.ma logic/equality.ma +TPTP/Veloci/GRP551-1.p.ma logic/equality.ma +TPTP/Veloci/GRP182-4.p.ma logic/equality.ma +TPTP/Veloci/GRP467-1.p.ma logic/equality.ma +TPTP/Veloci/LCL155-1.p.ma logic/equality.ma +TPTP/Veloci/COL086-1.p.ma logic/equality.ma +TPTP/Veloci/GRP614-1.p.ma logic/equality.ma +TPTP/Veloci/COL048-1.p.ma logic/equality.ma +TPTP/Veloci/GRP517-1.p.ma logic/equality.ma +TPTP/Veloci/GRP493-1.p.ma logic/equality.ma +TPTP/Veloci/LCL113-2.p.ma logic/equality.ma +TPTP/Veloci/BOO006-2.p.ma logic/equality.ma +TPTP/Veloci/GRP612-1.p.ma logic/equality.ma +TPTP/Veloci/GRP518-1.p.ma logic/equality.ma +TPTP/Veloci/GRP158-1.p.ma logic/equality.ma +TPTP/Veloci/BOO003-2.p.ma logic/equality.ma +TPTP/Veloci/BOO005-4.p.ma logic/equality.ma +TPTP/Veloci/GRP595-1.p.ma logic/equality.ma +TPTP/Veloci/COL060-2.p.ma logic/equality.ma +TPTP/Veloci/GRP494-1.p.ma logic/equality.ma +TPTP/Veloci/GRP163-1.p.ma logic/equality.ma +TPTP/Veloci/GRP168-2.p.ma logic/equality.ma +TPTP/Veloci/BOO075-1.p.ma logic/equality.ma +TPTP/Veloci/GRP605-1.p.ma logic/equality.ma +TPTP/Veloci/RNG007-4.p.ma logic/equality.ma +TPTP/Veloci/GRP486-1.p.ma logic/equality.ma +TPTP/Veloci/GRP149-1.p.ma logic/equality.ma +TPTP/Veloci/LDA007-3.p.ma logic/equality.ma +TPTP/Veloci/GRP568-1.p.ma logic/equality.ma +TPTP/Veloci/GRP189-2.p.ma logic/equality.ma +TPTP/Veloci/COL025-1.p.ma logic/equality.ma +TPTP/Veloci/BOO009-4.p.ma logic/equality.ma +TPTP/Veloci/ROB009-1.p.ma logic/equality.ma +TPTP/Veloci/GRP511-1.p.ma logic/equality.ma +TPTP/Veloci/GRP516-1.p.ma logic/equality.ma +TPTP/Veloci/GRP562-1.p.ma logic/equality.ma +TPTP/Veloci/GRP597-1.p.ma logic/equality.ma +TPTP/Veloci/GRP509-1.p.ma logic/equality.ma +TPTP/Veloci/LCL161-1.p.ma logic/equality.ma +TPTP/Veloci/BOO010-2.p.ma logic/equality.ma +TPTP/Veloci/RNG023-7.p.ma logic/equality.ma +TPTP/Veloci/GRP491-1.p.ma logic/equality.ma +TPTP/Veloci/GRP615-1.p.ma logic/equality.ma +TPTP/Veloci/GRP142-1.p.ma logic/equality.ma +TPTP/Veloci/GRP485-1.p.ma logic/equality.ma +TPTP/Veloci/GRP141-1.p.ma logic/equality.ma +TPTP/Veloci/GRP569-1.p.ma logic/equality.ma +TPTP/Veloci/LCL153-1.p.ma logic/equality.ma +TPTP/Veloci/GRP192-1.p.ma logic/equality.ma +TPTP/Veloci/BOO013-4.p.ma logic/equality.ma +TPTP/Veloci/BOO034-1.p.ma logic/equality.ma +TPTP/Veloci/BOO012-2.p.ma logic/equality.ma +TPTP/Veloci/COL007-1.p.ma logic/equality.ma +TPTP/Veloci/GRP547-1.p.ma logic/equality.ma +TPTP/Veloci/GRP510-1.p.ma logic/equality.ma +TPTP/Veloci/COL024-1.p.ma logic/equality.ma +TPTP/Veloci/LDA001-1.p.ma logic/equality.ma +TPTP/Veloci/GRP513-1.p.ma logic/equality.ma +TPTP/Veloci/LAT008-1.p.ma logic/equality.ma +TPTP/Veloci/GRP206-1.p.ma logic/equality.ma +TPTP/Veloci/GRP580-1.p.ma logic/equality.ma +TPTP/Veloci/GRP598-1.p.ma logic/equality.ma +TPTP/Veloci/COL063-6.p.ma logic/equality.ma +TPTP/Veloci/GRP153-1.p.ma logic/equality.ma +TPTP/Veloci/GRP151-1.p.ma logic/equality.ma +TPTP/Veloci/ROB010-1.p.ma logic/equality.ma +TPTP/Veloci/COL004-3.p.ma logic/equality.ma +TPTP/Veloci/GRP567-1.p.ma logic/equality.ma +TPTP/Veloci/LAT045-1.p.ma logic/equality.ma +TPTP/Veloci/GRP492-1.p.ma logic/equality.ma +TPTP/Veloci/LCL133-1.p.ma logic/equality.ma +TPTP/Veloci/COL063-4.p.ma logic/equality.ma +TPTP/Veloci/GRP463-1.p.ma logic/equality.ma +TPTP/Veloci/BOO004-2.p.ma logic/equality.ma +TPTP/Veloci/LCL134-1.p.ma logic/equality.ma +TPTP/Veloci/RNG023-6.p.ma logic/equality.ma +TPTP/Veloci/GRP487-1.p.ma logic/equality.ma +TPTP/Veloci/COL016-1.p.ma logic/equality.ma +TPTP/Veloci/GRP586-1.p.ma logic/equality.ma +TPTP/Veloci/ROB013-1.p.ma logic/equality.ma +TPTP/Veloci/LCL140-1.p.ma logic/equality.ma +TPTP/Veloci/LCL132-1.p.ma logic/equality.ma +TPTP/Veloci/BOO010-4.p.ma logic/equality.ma +TPTP/Veloci/COL014-1.p.ma logic/equality.ma +TPTP/Veloci/COL064-6.p.ma logic/equality.ma +TPTP/Veloci/GRP162-1.p.ma logic/equality.ma +TPTP/Veloci/GRP602-1.p.ma logic/equality.ma +TPTP/Veloci/ROB030-1.p.ma logic/equality.ma +TPTP/Veloci/GRP496-1.p.ma logic/equality.ma +TPTP/Veloci/COL058-2.p.ma logic/equality.ma +TPTP/Veloci/LCL112-2.p.ma logic/equality.ma +TPTP/Veloci/GRP484-1.p.ma logic/equality.ma +TPTP/Veloci/LAT034-1.p.ma logic/equality.ma +TPTP/Veloci/COL010-1.p.ma logic/equality.ma +TPTP/Veloci/GRP146-1.p.ma logic/equality.ma +TPTP/Veloci/GRP454-1.p.ma logic/equality.ma +TPTP/Veloci/BOO009-2.p.ma logic/equality.ma +TPTP/Veloci/LAT039-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/GRP143-1.p.ma logic/equality.ma +TPTP/Veloci/BOO004-4.p.ma logic/equality.ma +TPTP/Veloci/GRP604-1.p.ma logic/equality.ma +TPTP/Veloci/GRP488-1.p.ma logic/equality.ma +TPTP/Veloci/LAT040-1.p.ma logic/equality.ma +TPTP/Veloci/GRP182-1.p.ma logic/equality.ma +TPTP/Veloci/GRP543-1.p.ma logic/equality.ma +TPTP/Veloci/GRP118-1.p.ma logic/equality.ma +TPTP/Veloci/GRP514-1.p.ma logic/equality.ma +TPTP/Veloci/BOO003-4.p.ma logic/equality.ma +TPTP/Veloci/LCL157-1.p.ma logic/equality.ma +TPTP/Veloci/GRP542-1.p.ma logic/equality.ma +TPTP/Veloci/GRP182-3.p.ma logic/equality.ma +TPTP/Veloci/GRP117-1.p.ma logic/equality.ma +TPTP/Veloci/GRP606-1.p.ma logic/equality.ma +TPTP/Veloci/GRP456-1.p.ma logic/equality.ma +TPTP/Veloci/GRP549-1.p.ma logic/equality.ma +TPTP/Veloci/GRP154-1.p.ma logic/equality.ma +TPTP/Veloci/RNG008-4.p.ma logic/equality.ma +TPTP/Veloci/GRP561-1.p.ma logic/equality.ma +TPTP/Veloci/GRP139-1.p.ma logic/equality.ma +TPTP/Veloci/BOO018-4.p.ma logic/equality.ma +TPTP/Veloci/GRP144-1.p.ma logic/equality.ma +TPTP/Veloci/COL013-1.p.ma logic/equality.ma +TPTP/Veloci/BOO011-4.p.ma logic/equality.ma +TPTP/Veloci/LCL154-1.p.ma logic/equality.ma +TPTP/Veloci/GRP574-1.p.ma logic/equality.ma +TPTP/Veloci/GRP565-1.p.ma logic/equality.ma +TPTP/Veloci/GRP459-1.p.ma logic/equality.ma +TPTP/Veloci/GRP582-1.p.ma logic/equality.ma +TPTP/Veloci/GRP545-1.p.ma logic/equality.ma +TPTP/Veloci/LCL115-2.p.ma logic/equality.ma +TPTP/Veloci/GRP572-1.p.ma logic/equality.ma +TPTP/Veloci/GRP583-1.p.ma logic/equality.ma +TPTP/Veloci/GRP116-1.p.ma logic/equality.ma +TPTP/Veloci/COL064-9.p.ma logic/equality.ma +TPTP/Veloci/GRP560-1.p.ma logic/equality.ma +TPTP/Veloci/GRP145-1.p.ma logic/equality.ma +TPTP/Veloci/GRP160-1.p.ma logic/equality.ma +TPTP/Veloci/GRP581-1.p.ma logic/equality.ma +TPTP/Veloci/GRP001-2.p.ma logic/equality.ma +TPTP/Veloci/LAT033-1.p.ma logic/equality.ma +TPTP/Veloci/GRP023-2.p.ma logic/equality.ma +TPTP/Veloci/GRP001-4.p.ma logic/equality.ma +TPTP/Veloci/GRP603-1.p.ma logic/equality.ma +TPTP/Veloci/COL061-3.p.ma logic/equality.ma +TPTP/Veloci/COL064-5.p.ma logic/equality.ma +TPTP/Veloci/COL084-1.p.ma logic/equality.ma +TPTP/Veloci/GRP544-1.p.ma logic/equality.ma +TPTP/Veloci/GRP515-1.p.ma logic/equality.ma +TPTP/Veloci/GRP548-1.p.ma logic/equality.ma +TPTP/Veloci/COL022-1.p.ma logic/equality.ma +TPTP/Veloci/GRP188-2.p.ma logic/equality.ma +TPTP/Veloci/LCL164-1.p.ma logic/equality.ma +TPTP/Veloci/COL061-2.p.ma logic/equality.ma +TPTP/Veloci/GRP174-1.p.ma logic/equality.ma +TPTP/Veloci/GRP608-1.p.ma logic/equality.ma +TPTP/Veloci/GRP012-4.p.ma logic/equality.ma +TPTP/Veloci/BOO001-1.p.ma logic/equality.ma +TPTP/Veloci/GRP010-4.p.ma logic/equality.ma +TPTP/Veloci/COL018-1.p.ma logic/equality.ma +TPTP/Veloci/GRP458-1.p.ma logic/equality.ma +TPTP/Veloci/BOO071-1.p.ma logic/equality.ma +TPTP/Veloci/GRP497-1.p.ma logic/equality.ma +TPTP/Veloci/COL017-1.p.ma logic/equality.ma +TPTP/Veloci/COL060-3.p.ma logic/equality.ma +TPTP/Veloci/COL021-1.p.ma logic/equality.ma +TPTP/Veloci/GRP613-1.p.ma logic/equality.ma +TPTP/Veloci/GRP159-1.p.ma logic/equality.ma +TPTP/Veloci/LCL135-1.p.ma logic/equality.ma +TPTP/Veloci/GRP176-2.p.ma logic/equality.ma +TPTP/Veloci/GRP157-1.p.ma logic/equality.ma +TPTP/Veloci/GRP600-1.p.ma logic/equality.ma +TPTP/Veloci/COL064-7.p.ma logic/equality.ma +TPTP/Veloci/COL064-8.p.ma logic/equality.ma +TPTP/Veloci/GRP577-1.p.ma logic/equality.ma +TPTP/Veloci/GRP136-1.p.ma logic/equality.ma +TPTP/Veloci/BOO006-4.p.ma logic/equality.ma +TPTP/Veloci/GRP592-1.p.ma logic/equality.ma +TPTP/Veloci/GRP156-1.p.ma logic/equality.ma +TPTP/Veloci/GRP176-1.p.ma logic/equality.ma +TPTP/Veloci/RNG011-5.p.ma logic/equality.ma +TPTP/Veloci/GRP186-3.p.ma logic/equality.ma +TPTP/Veloci/GRP186-4.p.ma logic/equality.ma +TPTP/Veloci/GRP520-1.p.ma logic/equality.ma +TPTP/Veloci/COL058-3.p.ma logic/equality.ma +TPTP/Veloci/BOO069-1.p.ma logic/equality.ma +TPTP/Veloci/GRP022-2.p.ma logic/equality.ma +TPTP/Veloci/GRP155-1.p.ma logic/equality.ma +TPTP/Veloci/GRP188-1.p.ma logic/equality.ma +TPTP/Veloci/BOO016-2.p.ma logic/equality.ma +TPTP/Veloci/GRP498-1.p.ma logic/equality.ma +TPTP/Veloci/GRP590-1.p.ma logic/equality.ma +TPTP/Veloci/ROB002-1.p.ma logic/equality.ma +TPTP/Veloci/GRP152-1.p.ma logic/equality.ma +TPTP/Veloci/LCL110-2.p.ma logic/equality.ma +TPTP/Veloci/BOO017-2.p.ma logic/equality.ma +TPTP/Veloci/COL064-4.p.ma logic/equality.ma +TPTP/Veloci/LCL139-1.p.ma logic/equality.ma +TPTP/Veloci/COL063-2.p.ma logic/equality.ma +TPTP/Veloci/GRP182-2.p.ma logic/equality.ma +TPTP/Veloci/GRP490-1.p.ma logic/equality.ma +TPTP/Veloci/GRP115-1.p.ma logic/equality.ma +TPTP/Veloci/LCL141-1.p.ma logic/equality.ma +TPTP/Veloci/GRP564-1.p.ma logic/equality.ma +TPTP/Veloci/GRP481-1.p.ma logic/equality.ma +TPTP/Veloci/GRP455-1.p.ma logic/equality.ma +TPTP/Veloci/GRP550-1.p.ma logic/equality.ma +TPTP/Veloci/GRP599-1.p.ma logic/equality.ma +TPTP/Veloci/GRP596-1.p.ma logic/equality.ma +TPTP/Veloci/GRP460-1.p.ma logic/equality.ma +TPTP/Veloci/RNG024-7.p.ma logic/equality.ma +TPTP/Veloci/COL085-1.p.ma logic/equality.ma +TPTP/Veloci/LCL158-1.p.ma logic/equality.ma +TPTP/Veloci/GRP512-1.p.ma logic/equality.ma +TPTP/Veloci/GRP616-1.p.ma logic/equality.ma +TPTP/Veloci/GRP150-1.p.ma logic/equality.ma +TPTP/Veloci/GRP584-1.p.ma logic/equality.ma +TPTP/Veloci/COL064-3.p.ma logic/equality.ma +TPTP/Veloci/BOO013-2.p.ma logic/equality.ma +TPTP/Veloci/GRP566-1.p.ma logic/equality.ma +TPTP/Veloci/LCL156-1.p.ma logic/equality.ma +TPTP/Veloci/GRP573-1.p.ma logic/equality.ma +TPTP/Veloci/GRP541-1.p.ma logic/equality.ma +TPTP/Veloci/LCL114-2.p.ma logic/equality.ma +TPTP/Veloci/BOO011-2.p.ma logic/equality.ma +TPTP/Veloci/GRP546-1.p.ma logic/equality.ma +TPTP/Veloci/COL063-3.p.ma logic/equality.ma +TPTP/Veloci/GRP556-1.p.ma logic/equality.ma +TPTP/Veloci/GRP558-1.p.ma logic/equality.ma +TPTP/Veloci/GRP457-1.p.ma logic/equality.ma +coq.ma +datatypes/bool.ma +datatypes/constructors.ma +decidable_kit/list_aux.ma +list/list.ma +list/sort.ma +logic/connectives.ma +logic/equality.ma +nat/compare.ma +nat/div_and_mod.ma +nat/factorial.ma +nat/minus.ma +nat/nat.ma +nat/orders.ma +nat/primes.ma +nat/times.ma diff --git a/matita/tests/makefile b/matita/tests/makefile deleted file mode 100644 index c610118b6..000000000 --- a/matita/tests/makefile +++ /dev/null @@ -1,37 +0,0 @@ -H=@ - -RT_BASEDIR=../ -OPTIONS=-bench -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -ifneq "$(SRC)" "" - XXX=SRC=$(SRC) -endif - -all: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - diff --git a/matita/tests/root b/matita/tests/root new file mode 100644 index 000000000..175ea39f8 --- /dev/null +++ b/matita/tests/root @@ -0,0 +1,2 @@ +baseuri=cic:/matita/tests +include_paths=../legacy -- 2.39.2