From d4302f43737034a69bd475e5f46e8d126229375e Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 22 Mar 2008 11:17:17 +0000 Subject: [PATCH] moved dama/ and dama_didactic/ in contribs/dama/ the tests output should not change and history is preserved --- helm/software/matita/Makefile | 3 ++- helm/software/matita/contribs/dama/Makefile | 10 ++++++++++ helm/software/matita/contribs/dama/dama/Makefile | 16 ++++++++++++++++ .../dama}/dama/Q_is_orded_divisble_group.ma | 0 .../matita/{ => contribs/dama}/dama/TODO | 0 .../{ => contribs/dama}/dama/attic/fields.ma | 0 .../dama}/dama/attic/integration_algebras.ma | 0 .../dama}/dama/attic/ordered_fields_ch0.ma | 0 .../{ => contribs/dama}/dama/attic/reals.ma | 0 .../{ => contribs/dama}/dama/attic/rings.ma | 0 .../dama}/dama/attic/vector_spaces.ma | 0 .../dama/classical_pointfree/ordered_sets.ma | 0 .../dama/classical_pointfree/ordered_sets2.ma | 0 .../dama}/dama/classical_pointwise/sets.ma | 0 .../dama/classical_pointwise/sigma_algebra.ma | 0 .../dama}/dama/classical_pointwise/topology.ma | 0 .../dama}/dama/constructive_connectives.ma | 0 .../dama/constructive_higher_order_relations.ma | 0 .../dama/constructive_pointfree/lebesgue.ma | 0 .../matita/{ => contribs/dama}/dama/depends | 0 .../{ => contribs/dama}/dama/divisible_group.ma | 0 .../{ => contribs/dama}/dama/doc/DIMOSTRAZIONE | 0 .../dama}/dama/doc/NotaReticoli.pdf | 0 .../matita/{ => contribs/dama}/dama/excess.ma | 0 .../matita/{ => contribs/dama}/dama/group.ma | 0 .../matita/{ => contribs/dama}/dama/infsup.ma | 0 .../matita/{ => contribs/dama}/dama/lattice.ma | 0 .../matita/{ => contribs/dama}/dama/limit.ma | 0 .../{ => contribs/dama}/dama/metric_lattice.ma | 0 .../{ => contribs/dama}/dama/metric_space.ma | 0 .../dama}/dama/ordered_divisible_group.ma | 0 .../{ => contribs/dama}/dama/ordered_group.ma | 0 .../dama}/dama/premetric_lattice.ma | 0 .../dama}/dama/prevalued_lattice.ma | 0 .../matita/{ => contribs/dama}/dama/root | 0 .../matita/{ => contribs/dama}/dama/sandwich.ma | 0 .../dama}/dama/sandwich_corollary.ma | 0 .../matita/{ => contribs/dama}/dama/sequence.ma | 0 .../matita/{ => contribs/dama}/dama/tend.ma | 0 .../matita/contribs/dama/dama_didactic/Makefile | 16 ++++++++++++++++ .../{ => contribs/dama}/dama_didactic/bottom.ma | 0 .../{ => contribs/dama}/dama_didactic/depends | 0 .../{ => contribs/dama}/dama_didactic/deriv.ma | 0 .../dama}/dama_didactic/ex_deriv.ma | 0 .../{ => contribs/dama}/dama_didactic/ex_seq.ma | 0 .../{ => contribs/dama}/dama_didactic/reals.ma | 0 .../{ => contribs/dama}/dama_didactic/root | 2 +- .../dama}/dama_didactic/sequences.ma | 0 helm/software/matita/dama/Makefile | 10 ---------- helm/software/matita/dama_didactic/Makefile | 14 -------------- 50 files changed, 45 insertions(+), 26 deletions(-) create mode 100644 helm/software/matita/contribs/dama/Makefile create mode 100644 helm/software/matita/contribs/dama/dama/Makefile rename helm/software/matita/{ => contribs/dama}/dama/Q_is_orded_divisble_group.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/TODO (100%) rename helm/software/matita/{ => contribs/dama}/dama/attic/fields.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/attic/integration_algebras.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/attic/ordered_fields_ch0.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/attic/reals.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/attic/rings.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/attic/vector_spaces.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/classical_pointfree/ordered_sets.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/classical_pointfree/ordered_sets2.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/classical_pointwise/sets.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/classical_pointwise/sigma_algebra.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/classical_pointwise/topology.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/constructive_connectives.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/constructive_higher_order_relations.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/constructive_pointfree/lebesgue.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/depends (100%) rename helm/software/matita/{ => contribs/dama}/dama/divisible_group.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/doc/DIMOSTRAZIONE (100%) rename helm/software/matita/{ => contribs/dama}/dama/doc/NotaReticoli.pdf (100%) rename helm/software/matita/{ => contribs/dama}/dama/excess.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/group.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/infsup.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/lattice.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/limit.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/metric_lattice.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/metric_space.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/ordered_divisible_group.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/ordered_group.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/premetric_lattice.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/prevalued_lattice.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/root (100%) rename helm/software/matita/{ => contribs/dama}/dama/sandwich.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/sandwich_corollary.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/sequence.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama/tend.ma (100%) create mode 100644 helm/software/matita/contribs/dama/dama_didactic/Makefile rename helm/software/matita/{ => contribs/dama}/dama_didactic/bottom.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama_didactic/depends (100%) rename helm/software/matita/{ => contribs/dama}/dama_didactic/deriv.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama_didactic/ex_deriv.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama_didactic/ex_seq.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama_didactic/reals.ma (100%) rename helm/software/matita/{ => contribs/dama}/dama_didactic/root (50%) rename helm/software/matita/{ => contribs/dama}/dama_didactic/sequences.ma (100%) delete mode 100644 helm/software/matita/dama/Makefile delete mode 100644 helm/software/matita/dama_didactic/Makefile diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile index a872f3194..eae880741 100644 --- a/helm/software/matita/Makefile +++ b/helm/software/matita/Makefile @@ -183,7 +183,8 @@ TEST_DIRS = \ legacy \ library \ tests \ - dama \ + contribs/dama/dama \ + contribs/assembly \ contribs/CoRN \ contribs/RELATIONAL \ contribs/LOGIC \ diff --git a/helm/software/matita/contribs/dama/Makefile b/helm/software/matita/contribs/dama/Makefile new file mode 100644 index 000000000..c2cc976d4 --- /dev/null +++ b/helm/software/matita/contribs/dama/Makefile @@ -0,0 +1,10 @@ +GOALS = all opt clean clean.opt + +DEVELS = dama dama_didactic + +$(GOALS): + @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) + +.PHONY: (GOALS) + +.SUFFIXES: diff --git a/helm/software/matita/contribs/dama/dama/Makefile b/helm/software/matita/contribs/dama/dama/Makefile new file mode 100644 index 000000000..d40c9e674 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama/Makefile @@ -0,0 +1,16 @@ +include ../../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)../matitac +$(DIR).opt opt all.opt: + $(BIN)../matitac.opt +clean: + $(BIN)../matitaclean +clean.opt: + $(BIN)../matitaclean.opt +depend: + $(BIN)../matitadep +depend.opt: + $(BIN)../matitadep.opt diff --git a/helm/software/matita/dama/Q_is_orded_divisble_group.ma b/helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma similarity index 100% rename from helm/software/matita/dama/Q_is_orded_divisble_group.ma rename to helm/software/matita/contribs/dama/dama/Q_is_orded_divisble_group.ma diff --git a/helm/software/matita/dama/TODO b/helm/software/matita/contribs/dama/dama/TODO similarity index 100% rename from helm/software/matita/dama/TODO rename to helm/software/matita/contribs/dama/dama/TODO diff --git a/helm/software/matita/dama/attic/fields.ma b/helm/software/matita/contribs/dama/dama/attic/fields.ma similarity index 100% rename from helm/software/matita/dama/attic/fields.ma rename to helm/software/matita/contribs/dama/dama/attic/fields.ma diff --git a/helm/software/matita/dama/attic/integration_algebras.ma b/helm/software/matita/contribs/dama/dama/attic/integration_algebras.ma similarity index 100% rename from helm/software/matita/dama/attic/integration_algebras.ma rename to helm/software/matita/contribs/dama/dama/attic/integration_algebras.ma diff --git a/helm/software/matita/dama/attic/ordered_fields_ch0.ma b/helm/software/matita/contribs/dama/dama/attic/ordered_fields_ch0.ma similarity index 100% rename from helm/software/matita/dama/attic/ordered_fields_ch0.ma rename to helm/software/matita/contribs/dama/dama/attic/ordered_fields_ch0.ma diff --git a/helm/software/matita/dama/attic/reals.ma b/helm/software/matita/contribs/dama/dama/attic/reals.ma similarity index 100% rename from helm/software/matita/dama/attic/reals.ma rename to helm/software/matita/contribs/dama/dama/attic/reals.ma diff --git a/helm/software/matita/dama/attic/rings.ma b/helm/software/matita/contribs/dama/dama/attic/rings.ma similarity index 100% rename from helm/software/matita/dama/attic/rings.ma rename to helm/software/matita/contribs/dama/dama/attic/rings.ma diff --git a/helm/software/matita/dama/attic/vector_spaces.ma b/helm/software/matita/contribs/dama/dama/attic/vector_spaces.ma similarity index 100% rename from helm/software/matita/dama/attic/vector_spaces.ma rename to helm/software/matita/contribs/dama/dama/attic/vector_spaces.ma diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets.ma b/helm/software/matita/contribs/dama/dama/classical_pointfree/ordered_sets.ma similarity index 100% rename from helm/software/matita/dama/classical_pointfree/ordered_sets.ma rename to helm/software/matita/contribs/dama/dama/classical_pointfree/ordered_sets.ma diff --git a/helm/software/matita/dama/classical_pointfree/ordered_sets2.ma b/helm/software/matita/contribs/dama/dama/classical_pointfree/ordered_sets2.ma similarity index 100% rename from helm/software/matita/dama/classical_pointfree/ordered_sets2.ma rename to helm/software/matita/contribs/dama/dama/classical_pointfree/ordered_sets2.ma diff --git a/helm/software/matita/dama/classical_pointwise/sets.ma b/helm/software/matita/contribs/dama/dama/classical_pointwise/sets.ma similarity index 100% rename from helm/software/matita/dama/classical_pointwise/sets.ma rename to helm/software/matita/contribs/dama/dama/classical_pointwise/sets.ma diff --git a/helm/software/matita/dama/classical_pointwise/sigma_algebra.ma b/helm/software/matita/contribs/dama/dama/classical_pointwise/sigma_algebra.ma similarity index 100% rename from helm/software/matita/dama/classical_pointwise/sigma_algebra.ma rename to helm/software/matita/contribs/dama/dama/classical_pointwise/sigma_algebra.ma diff --git a/helm/software/matita/dama/classical_pointwise/topology.ma b/helm/software/matita/contribs/dama/dama/classical_pointwise/topology.ma similarity index 100% rename from helm/software/matita/dama/classical_pointwise/topology.ma rename to helm/software/matita/contribs/dama/dama/classical_pointwise/topology.ma diff --git a/helm/software/matita/dama/constructive_connectives.ma b/helm/software/matita/contribs/dama/dama/constructive_connectives.ma similarity index 100% rename from helm/software/matita/dama/constructive_connectives.ma rename to helm/software/matita/contribs/dama/dama/constructive_connectives.ma diff --git a/helm/software/matita/dama/constructive_higher_order_relations.ma b/helm/software/matita/contribs/dama/dama/constructive_higher_order_relations.ma similarity index 100% rename from helm/software/matita/dama/constructive_higher_order_relations.ma rename to helm/software/matita/contribs/dama/dama/constructive_higher_order_relations.ma diff --git a/helm/software/matita/dama/constructive_pointfree/lebesgue.ma b/helm/software/matita/contribs/dama/dama/constructive_pointfree/lebesgue.ma similarity index 100% rename from helm/software/matita/dama/constructive_pointfree/lebesgue.ma rename to helm/software/matita/contribs/dama/dama/constructive_pointfree/lebesgue.ma diff --git a/helm/software/matita/dama/depends b/helm/software/matita/contribs/dama/dama/depends similarity index 100% rename from helm/software/matita/dama/depends rename to helm/software/matita/contribs/dama/dama/depends diff --git a/helm/software/matita/dama/divisible_group.ma b/helm/software/matita/contribs/dama/dama/divisible_group.ma similarity index 100% rename from helm/software/matita/dama/divisible_group.ma rename to helm/software/matita/contribs/dama/dama/divisible_group.ma diff --git a/helm/software/matita/dama/doc/DIMOSTRAZIONE b/helm/software/matita/contribs/dama/dama/doc/DIMOSTRAZIONE similarity index 100% rename from helm/software/matita/dama/doc/DIMOSTRAZIONE rename to helm/software/matita/contribs/dama/dama/doc/DIMOSTRAZIONE diff --git a/helm/software/matita/dama/doc/NotaReticoli.pdf b/helm/software/matita/contribs/dama/dama/doc/NotaReticoli.pdf similarity index 100% rename from helm/software/matita/dama/doc/NotaReticoli.pdf rename to helm/software/matita/contribs/dama/dama/doc/NotaReticoli.pdf diff --git a/helm/software/matita/dama/excess.ma b/helm/software/matita/contribs/dama/dama/excess.ma similarity index 100% rename from helm/software/matita/dama/excess.ma rename to helm/software/matita/contribs/dama/dama/excess.ma diff --git a/helm/software/matita/dama/group.ma b/helm/software/matita/contribs/dama/dama/group.ma similarity index 100% rename from helm/software/matita/dama/group.ma rename to helm/software/matita/contribs/dama/dama/group.ma diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/contribs/dama/dama/infsup.ma similarity index 100% rename from helm/software/matita/dama/infsup.ma rename to helm/software/matita/contribs/dama/dama/infsup.ma diff --git a/helm/software/matita/dama/lattice.ma b/helm/software/matita/contribs/dama/dama/lattice.ma similarity index 100% rename from helm/software/matita/dama/lattice.ma rename to helm/software/matita/contribs/dama/dama/lattice.ma diff --git a/helm/software/matita/dama/limit.ma b/helm/software/matita/contribs/dama/dama/limit.ma similarity index 100% rename from helm/software/matita/dama/limit.ma rename to helm/software/matita/contribs/dama/dama/limit.ma diff --git a/helm/software/matita/dama/metric_lattice.ma b/helm/software/matita/contribs/dama/dama/metric_lattice.ma similarity index 100% rename from helm/software/matita/dama/metric_lattice.ma rename to helm/software/matita/contribs/dama/dama/metric_lattice.ma diff --git a/helm/software/matita/dama/metric_space.ma b/helm/software/matita/contribs/dama/dama/metric_space.ma similarity index 100% rename from helm/software/matita/dama/metric_space.ma rename to helm/software/matita/contribs/dama/dama/metric_space.ma diff --git a/helm/software/matita/dama/ordered_divisible_group.ma b/helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma similarity index 100% rename from helm/software/matita/dama/ordered_divisible_group.ma rename to helm/software/matita/contribs/dama/dama/ordered_divisible_group.ma diff --git a/helm/software/matita/dama/ordered_group.ma b/helm/software/matita/contribs/dama/dama/ordered_group.ma similarity index 100% rename from helm/software/matita/dama/ordered_group.ma rename to helm/software/matita/contribs/dama/dama/ordered_group.ma diff --git a/helm/software/matita/dama/premetric_lattice.ma b/helm/software/matita/contribs/dama/dama/premetric_lattice.ma similarity index 100% rename from helm/software/matita/dama/premetric_lattice.ma rename to helm/software/matita/contribs/dama/dama/premetric_lattice.ma diff --git a/helm/software/matita/dama/prevalued_lattice.ma b/helm/software/matita/contribs/dama/dama/prevalued_lattice.ma similarity index 100% rename from helm/software/matita/dama/prevalued_lattice.ma rename to helm/software/matita/contribs/dama/dama/prevalued_lattice.ma diff --git a/helm/software/matita/dama/root b/helm/software/matita/contribs/dama/dama/root similarity index 100% rename from helm/software/matita/dama/root rename to helm/software/matita/contribs/dama/dama/root diff --git a/helm/software/matita/dama/sandwich.ma b/helm/software/matita/contribs/dama/dama/sandwich.ma similarity index 100% rename from helm/software/matita/dama/sandwich.ma rename to helm/software/matita/contribs/dama/dama/sandwich.ma diff --git a/helm/software/matita/dama/sandwich_corollary.ma b/helm/software/matita/contribs/dama/dama/sandwich_corollary.ma similarity index 100% rename from helm/software/matita/dama/sandwich_corollary.ma rename to helm/software/matita/contribs/dama/dama/sandwich_corollary.ma diff --git a/helm/software/matita/dama/sequence.ma b/helm/software/matita/contribs/dama/dama/sequence.ma similarity index 100% rename from helm/software/matita/dama/sequence.ma rename to helm/software/matita/contribs/dama/dama/sequence.ma diff --git a/helm/software/matita/dama/tend.ma b/helm/software/matita/contribs/dama/dama/tend.ma similarity index 100% rename from helm/software/matita/dama/tend.ma rename to helm/software/matita/contribs/dama/dama/tend.ma diff --git a/helm/software/matita/contribs/dama/dama_didactic/Makefile b/helm/software/matita/contribs/dama/dama_didactic/Makefile new file mode 100644 index 000000000..d40c9e674 --- /dev/null +++ b/helm/software/matita/contribs/dama/dama_didactic/Makefile @@ -0,0 +1,16 @@ +include ../../Makefile.defs + +DIR=$(shell basename $$PWD) + +$(DIR) all: + $(BIN)../matitac +$(DIR).opt opt all.opt: + $(BIN)../matitac.opt +clean: + $(BIN)../matitaclean +clean.opt: + $(BIN)../matitaclean.opt +depend: + $(BIN)../matitadep +depend.opt: + $(BIN)../matitadep.opt diff --git a/helm/software/matita/dama_didactic/bottom.ma b/helm/software/matita/contribs/dama/dama_didactic/bottom.ma similarity index 100% rename from helm/software/matita/dama_didactic/bottom.ma rename to helm/software/matita/contribs/dama/dama_didactic/bottom.ma diff --git a/helm/software/matita/dama_didactic/depends b/helm/software/matita/contribs/dama/dama_didactic/depends similarity index 100% rename from helm/software/matita/dama_didactic/depends rename to helm/software/matita/contribs/dama/dama_didactic/depends diff --git a/helm/software/matita/dama_didactic/deriv.ma b/helm/software/matita/contribs/dama/dama_didactic/deriv.ma similarity index 100% rename from helm/software/matita/dama_didactic/deriv.ma rename to helm/software/matita/contribs/dama/dama_didactic/deriv.ma diff --git a/helm/software/matita/dama_didactic/ex_deriv.ma b/helm/software/matita/contribs/dama/dama_didactic/ex_deriv.ma similarity index 100% rename from helm/software/matita/dama_didactic/ex_deriv.ma rename to helm/software/matita/contribs/dama/dama_didactic/ex_deriv.ma diff --git a/helm/software/matita/dama_didactic/ex_seq.ma b/helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma similarity index 100% rename from helm/software/matita/dama_didactic/ex_seq.ma rename to helm/software/matita/contribs/dama/dama_didactic/ex_seq.ma diff --git a/helm/software/matita/dama_didactic/reals.ma b/helm/software/matita/contribs/dama/dama_didactic/reals.ma similarity index 100% rename from helm/software/matita/dama_didactic/reals.ma rename to helm/software/matita/contribs/dama/dama_didactic/reals.ma diff --git a/helm/software/matita/dama_didactic/root b/helm/software/matita/contribs/dama/dama_didactic/root similarity index 50% rename from helm/software/matita/dama_didactic/root rename to helm/software/matita/contribs/dama/dama_didactic/root index 2d3086b02..a9ae19c08 100644 --- a/helm/software/matita/dama_didactic/root +++ b/helm/software/matita/contribs/dama/dama_didactic/root @@ -1,2 +1,2 @@ baseuri=cic:/matita/didactic -include_paths=../tests +include_paths=../../../tests diff --git a/helm/software/matita/dama_didactic/sequences.ma b/helm/software/matita/contribs/dama/dama_didactic/sequences.ma similarity index 100% rename from helm/software/matita/dama_didactic/sequences.ma rename to helm/software/matita/contribs/dama/dama_didactic/sequences.ma diff --git a/helm/software/matita/dama/Makefile b/helm/software/matita/dama/Makefile deleted file mode 100644 index 2eefa0cbd..000000000 --- a/helm/software/matita/dama/Makefile +++ /dev/null @@ -1,10 +0,0 @@ -DIR=$(shell basename $$PWD) - -$(DIR) all: - ../matitac -$(DIR).opt opt all.opt: - ../matitac.opt -clean: - ../matitaclean -clean.opt: - ../matitaclean.opt diff --git a/helm/software/matita/dama_didactic/Makefile b/helm/software/matita/dama_didactic/Makefile deleted file mode 100644 index cce033fc0..000000000 --- a/helm/software/matita/dama_didactic/Makefile +++ /dev/null @@ -1,14 +0,0 @@ -DIR=$(shell basename $$PWD) - -$(DIR) all: - ../matitac -$(DIR).opt opt all.opt: - ../matitac.opt -clean: - ../matitaclean -clean.opt: - ../matitaclean.opt -depend: - ../matitadep -depend.opt: - ../matitadep.opt -- 2.39.2