From 661ffd4d7c77fce52fb2f2d96f1737be424af3f1 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 22 Mar 2008 11:01:57 +0000 Subject: [PATCH] freescale moved under contribs. contribs made relocatable since all internal Makefile include a Makefile.defs defining where to find matita* tests should not be affected since the output of the compilation is the same and the URIs are the same --- .../matita/contribs/LAMBDA-TYPES/Makefile | 30 ++-- helm/software/matita/contribs/LOGIC/Makefile | 14 +- helm/software/matita/contribs/Makefile | 2 +- helm/software/matita/contribs/Makefile.defs | 1 + .../matita/contribs/RELATIONAL/Makefile | 14 +- .../matita/contribs/assembly/Makefile | 16 ++ .../software/matita/contribs/assembly/depends | 33 ++++ .../assembly}/freescale/aux_bases.ma | 0 .../assembly}/freescale/byte8.ma | 0 .../assembly}/freescale/doc/aurei.txt | 0 .../assembly}/freescale/doc/daa.txt | 0 .../assembly}/freescale/doc/freescale.txt | 0 .../assembly}/freescale/doc/ordinamento.txt | 0 .../freescale/doc/ordine_compilazione.txt | 0 .../assembly}/freescale/doc/reverse.txt | 0 .../assembly}/freescale/exadecim.ma | 0 .../assembly}/freescale/extra.ma | 0 .../assembly}/freescale/load_write.ma | 0 .../assembly}/freescale/medium_tests.ma | 0 .../freescale/medium_tests_lemmas.ma | 0 .../assembly}/freescale/medium_tests_tools.ma | 0 .../assembly}/freescale/memory_abs.ma | 0 .../assembly}/freescale/memory_bits.ma | 0 .../assembly}/freescale/memory_func.ma | 0 .../assembly}/freescale/memory_struct.ma | 0 .../assembly}/freescale/memory_trees.ma | 0 .../assembly}/freescale/micro_tests.ma | 0 .../assembly}/freescale/model.ma | 0 .../assembly}/freescale/multivm.ma | 0 .../assembly}/freescale/opcode.ma | 0 .../assembly}/freescale/status.ma | 0 .../assembly}/freescale/table_HC05.ma | 0 .../assembly}/freescale/table_HC05_tests.ma | 0 .../assembly}/freescale/table_HC08.ma | 0 .../assembly}/freescale/table_HC08_tests.ma | 0 .../assembly}/freescale/table_HCS08.ma | 0 .../assembly}/freescale/table_HCS08_tests.ma | 0 .../assembly}/freescale/table_RS08.ma | 0 .../assembly}/freescale/table_RS08_tests.ma | 0 .../assembly}/freescale/tests.old | 0 .../assembly}/freescale/translation.ma | 0 .../assembly}/freescale/word16.ma | 0 helm/software/matita/contribs/assembly/root | 1 + helm/software/matita/library/depends | 156 +++++++----------- 44 files changed, 148 insertions(+), 119 deletions(-) create mode 100644 helm/software/matita/contribs/Makefile.defs create mode 100644 helm/software/matita/contribs/assembly/Makefile create mode 100644 helm/software/matita/contribs/assembly/depends rename helm/software/matita/{library => contribs/assembly}/freescale/aux_bases.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/byte8.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/doc/aurei.txt (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/doc/daa.txt (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/doc/freescale.txt (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/doc/ordinamento.txt (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/doc/ordine_compilazione.txt (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/doc/reverse.txt (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/exadecim.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/extra.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/load_write.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/medium_tests.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/medium_tests_lemmas.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/medium_tests_tools.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/memory_abs.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/memory_bits.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/memory_func.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/memory_struct.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/memory_trees.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/micro_tests.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/model.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/multivm.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/opcode.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/status.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_HC05.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_HC05_tests.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_HC08.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_HC08_tests.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_HCS08.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_HCS08_tests.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_RS08.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/table_RS08_tests.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/tests.old (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/translation.ma (100%) rename helm/software/matita/{library => contribs/assembly}/freescale/word16.ma (100%) create mode 100644 helm/software/matita/contribs/assembly/root diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile index 754dde621..7edd28817 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile @@ -1,3 +1,5 @@ +include ../Makefile.defs + H=@ MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass @@ -15,45 +17,45 @@ $(DIR).opt opt all.opt: depends $(H)$(MAKE) H=$(H) --no-print-directory build.opt build: $(MAS) - $(H)echo Legacy-2/theory.ma `../../matitadep.opt -stdout Legacy-2/theory.ma` >> depends -# $(H)echo Base-2/theory.ma `../../matitadep.opt -stdout Base-2/theory.ma` >> depends - $(H)../../matitac $(MATITAOPTIONS) 2> /dev/null + $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends +# $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends + $(H)$(BIN)matitac $(MATITAOPTIONS) 2> /dev/null $(H)rm depends build.opt: $(MAS) - $(H)echo Legacy-2/theory.ma `../../matitadep.opt -stdout Legacy-2/theory.ma` >> depends -# $(H)echo Base-2/theory.ma `../../matitadep.opt -stdout Base-2/theory.ma` >> depends - $(H)../../matitac.opt $(MATITAOPTIONS) 2> /dev/null + $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends +# $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends + $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2> /dev/null $(H)rm depends clean: - $(H)../../matitaclean $(MATITAOPTIONS) + $(H)$(BIN)matitaclean $(MATITAOPTIONS) $(H)rm -f $(MAS) depends clean.opt: - $(H)../../matitaclean.opt $(MATITAOPTIONS) + $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(H)rm -f $(MAS) depends clean.ma: - $(H)../../matitaclean.opt $(MATITAOPTIONS) $(MAS) + $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS) $(MAS) $(H)rm -f $(MAS) depends depend: @echo matitadep - $(H)../../matitadep $(foreach FILE,$(XMAS),-exclude $(FILE)) + $(H)$(BIN)matitadep $(foreach FILE,$(XMAS),-exclude $(FILE)) $(H)cat Legacy-2/depends >> depends # Base-2/depends depend.opt: @echo matitadep.opt - $(H)../../matitadep.opt $(foreach FILE,$(XMAS),-exclude $(FILE)) + $(H)$(BIN)matitadep.opt $(foreach FILE,$(XMAS),-exclude $(FILE)) $(H)cat Legacy-2/depends >> depends # Base-2/depends depends: depend.opt %.ma: %.mma - $(H)../../matitac.opt $(MATITAOPTIONS) $(word 3,$(shell grep -h $< */depends)) `../../matitadep.opt -stdout $<` 2> /dev/null - $(H)../../matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null - $(H)echo $@ `../../matitadep.opt -stdout $@` >> depends + $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $(word 3,$(shell grep -h $< */depends)) `$(BIN)matitadep.opt -stdout $<` 2> /dev/null + $(H)$(BIN)matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null + $(H)echo $@ `$(BIN)matitadep.opt -stdout $@` >> depends include Legacy-2/.depend # include Base-2/.depend diff --git a/helm/software/matita/contribs/LOGIC/Makefile b/helm/software/matita/contribs/LOGIC/Makefile index c925bddff..a3e891435 100644 --- a/helm/software/matita/contribs/LOGIC/Makefile +++ b/helm/software/matita/contribs/LOGIC/Makefile @@ -1,14 +1,16 @@ +include ../Makefile.defs + DIR=$(shell basename $$PWD) $(DIR) all: - ../../matitac + $(BIN)matitac $(DIR).opt opt all.opt: - ../../matitac.opt + $(BIN)matitac.opt clean: - ../../matitaclean + $(BIN)matitaclean clean.opt: - ../../matitaclean.opt + $(BIN)matitaclean.opt depend: - ../../matitadep + $(BIN)matitadep depend.opt: - ../../matitadep.opt + $(BIN)matitadep.opt diff --git a/helm/software/matita/contribs/Makefile b/helm/software/matita/contribs/Makefile index 7e4aa7046..97eb363c9 100644 --- a/helm/software/matita/contribs/Makefile +++ b/helm/software/matita/contribs/Makefile @@ -1,6 +1,6 @@ GOALS = all opt clean clean.opt -DEVELS = RELATIONAL LOGIC LAMBDA-TYPES +DEVELS = RELATIONAL LOGIC LAMBDA-TYPES assembly $(GOALS): @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) diff --git a/helm/software/matita/contribs/Makefile.defs b/helm/software/matita/contribs/Makefile.defs new file mode 100644 index 000000000..5525a9f6b --- /dev/null +++ b/helm/software/matita/contribs/Makefile.defs @@ -0,0 +1 @@ +BIN=../../ diff --git a/helm/software/matita/contribs/RELATIONAL/Makefile b/helm/software/matita/contribs/RELATIONAL/Makefile index c925bddff..a3e891435 100644 --- a/helm/software/matita/contribs/RELATIONAL/Makefile +++ b/helm/software/matita/contribs/RELATIONAL/Makefile @@ -1,14 +1,16 @@ +include ../Makefile.defs + DIR=$(shell basename $$PWD) $(DIR) all: - ../../matitac + $(BIN)matitac $(DIR).opt opt all.opt: - ../../matitac.opt + $(BIN)matitac.opt clean: - ../../matitaclean + $(BIN)matitaclean clean.opt: - ../../matitaclean.opt + $(BIN)matitaclean.opt depend: - ../../matitadep + $(BIN)matitadep depend.opt: - ../../matitadep.opt + $(BIN)matitadep.opt diff --git a/helm/software/matita/contribs/assembly/Makefile b/helm/software/matita/contribs/assembly/Makefile new file mode 100644 index 000000000..a3e891435 --- /dev/null +++ b/helm/software/matita/contribs/assembly/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/contribs/assembly/depends b/helm/software/matita/contribs/assembly/depends new file mode 100644 index 000000000..049af9f67 --- /dev/null +++ b/helm/software/matita/contribs/assembly/depends @@ -0,0 +1,33 @@ +freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma +freescale/table_RS08_tests.ma freescale/table_RS08.ma +freescale/table_HCS08.ma freescale/opcode.ma +freescale/table_RS08.ma freescale/opcode.ma +freescale/memory_trees.ma freescale/memory_struct.ma +freescale/multivm.ma freescale/load_write.ma +freescale/opcode.ma freescale/aux_bases.ma +freescale/memory_func.ma freescale/memory_struct.ma +freescale/micro_tests.ma freescale/multivm.ma +freescale/exadecim.ma freescale/extra.ma +freescale/table_HC08.ma freescale/opcode.ma +freescale/table_HC05.ma freescale/opcode.ma +freescale/memory_bits.ma freescale/memory_trees.ma +freescale/word16.ma freescale/byte8.ma +freescale/table_HC08_tests.ma freescale/table_HC08.ma +freescale/table_HC05_tests.ma freescale/table_HC05.ma +freescale/model.ma freescale/status.ma +freescale/medium_tests.ma freescale/medium_tests_lemmas.ma +freescale/medium_tests_tools.ma freescale/multivm.ma +freescale/load_write.ma freescale/model.ma +freescale/memory_struct.ma freescale/translation.ma +freescale/table_HCS08_tests.ma freescale/table_HCS08.ma +freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma +freescale/extra.ma datatypes/constructors.ma list/list.ma logic/connectives.ma nat/div_and_mod.ma nat/primes.ma +freescale/aux_bases.ma freescale/word16.ma +freescale/medium_tests_lemmas.ma freescale/medium_tests_tools.ma +freescale/status.ma freescale/memory_abs.ma +freescale/byte8.ma freescale/exadecim.ma +datatypes/constructors.ma +list/list.ma +logic/connectives.ma +nat/div_and_mod.ma +nat/primes.ma diff --git a/helm/software/matita/library/freescale/aux_bases.ma b/helm/software/matita/contribs/assembly/freescale/aux_bases.ma similarity index 100% rename from helm/software/matita/library/freescale/aux_bases.ma rename to helm/software/matita/contribs/assembly/freescale/aux_bases.ma diff --git a/helm/software/matita/library/freescale/byte8.ma b/helm/software/matita/contribs/assembly/freescale/byte8.ma similarity index 100% rename from helm/software/matita/library/freescale/byte8.ma rename to helm/software/matita/contribs/assembly/freescale/byte8.ma diff --git a/helm/software/matita/library/freescale/doc/aurei.txt b/helm/software/matita/contribs/assembly/freescale/doc/aurei.txt similarity index 100% rename from helm/software/matita/library/freescale/doc/aurei.txt rename to helm/software/matita/contribs/assembly/freescale/doc/aurei.txt diff --git a/helm/software/matita/library/freescale/doc/daa.txt b/helm/software/matita/contribs/assembly/freescale/doc/daa.txt similarity index 100% rename from helm/software/matita/library/freescale/doc/daa.txt rename to helm/software/matita/contribs/assembly/freescale/doc/daa.txt diff --git a/helm/software/matita/library/freescale/doc/freescale.txt b/helm/software/matita/contribs/assembly/freescale/doc/freescale.txt similarity index 100% rename from helm/software/matita/library/freescale/doc/freescale.txt rename to helm/software/matita/contribs/assembly/freescale/doc/freescale.txt diff --git a/helm/software/matita/library/freescale/doc/ordinamento.txt b/helm/software/matita/contribs/assembly/freescale/doc/ordinamento.txt similarity index 100% rename from helm/software/matita/library/freescale/doc/ordinamento.txt rename to helm/software/matita/contribs/assembly/freescale/doc/ordinamento.txt diff --git a/helm/software/matita/library/freescale/doc/ordine_compilazione.txt b/helm/software/matita/contribs/assembly/freescale/doc/ordine_compilazione.txt similarity index 100% rename from helm/software/matita/library/freescale/doc/ordine_compilazione.txt rename to helm/software/matita/contribs/assembly/freescale/doc/ordine_compilazione.txt diff --git a/helm/software/matita/library/freescale/doc/reverse.txt b/helm/software/matita/contribs/assembly/freescale/doc/reverse.txt similarity index 100% rename from helm/software/matita/library/freescale/doc/reverse.txt rename to helm/software/matita/contribs/assembly/freescale/doc/reverse.txt diff --git a/helm/software/matita/library/freescale/exadecim.ma b/helm/software/matita/contribs/assembly/freescale/exadecim.ma similarity index 100% rename from helm/software/matita/library/freescale/exadecim.ma rename to helm/software/matita/contribs/assembly/freescale/exadecim.ma diff --git a/helm/software/matita/library/freescale/extra.ma b/helm/software/matita/contribs/assembly/freescale/extra.ma similarity index 100% rename from helm/software/matita/library/freescale/extra.ma rename to helm/software/matita/contribs/assembly/freescale/extra.ma diff --git a/helm/software/matita/library/freescale/load_write.ma b/helm/software/matita/contribs/assembly/freescale/load_write.ma similarity index 100% rename from helm/software/matita/library/freescale/load_write.ma rename to helm/software/matita/contribs/assembly/freescale/load_write.ma diff --git a/helm/software/matita/library/freescale/medium_tests.ma b/helm/software/matita/contribs/assembly/freescale/medium_tests.ma similarity index 100% rename from helm/software/matita/library/freescale/medium_tests.ma rename to helm/software/matita/contribs/assembly/freescale/medium_tests.ma diff --git a/helm/software/matita/library/freescale/medium_tests_lemmas.ma b/helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma similarity index 100% rename from helm/software/matita/library/freescale/medium_tests_lemmas.ma rename to helm/software/matita/contribs/assembly/freescale/medium_tests_lemmas.ma diff --git a/helm/software/matita/library/freescale/medium_tests_tools.ma b/helm/software/matita/contribs/assembly/freescale/medium_tests_tools.ma similarity index 100% rename from helm/software/matita/library/freescale/medium_tests_tools.ma rename to helm/software/matita/contribs/assembly/freescale/medium_tests_tools.ma diff --git a/helm/software/matita/library/freescale/memory_abs.ma b/helm/software/matita/contribs/assembly/freescale/memory_abs.ma similarity index 100% rename from helm/software/matita/library/freescale/memory_abs.ma rename to helm/software/matita/contribs/assembly/freescale/memory_abs.ma diff --git a/helm/software/matita/library/freescale/memory_bits.ma b/helm/software/matita/contribs/assembly/freescale/memory_bits.ma similarity index 100% rename from helm/software/matita/library/freescale/memory_bits.ma rename to helm/software/matita/contribs/assembly/freescale/memory_bits.ma diff --git a/helm/software/matita/library/freescale/memory_func.ma b/helm/software/matita/contribs/assembly/freescale/memory_func.ma similarity index 100% rename from helm/software/matita/library/freescale/memory_func.ma rename to helm/software/matita/contribs/assembly/freescale/memory_func.ma diff --git a/helm/software/matita/library/freescale/memory_struct.ma b/helm/software/matita/contribs/assembly/freescale/memory_struct.ma similarity index 100% rename from helm/software/matita/library/freescale/memory_struct.ma rename to helm/software/matita/contribs/assembly/freescale/memory_struct.ma diff --git a/helm/software/matita/library/freescale/memory_trees.ma b/helm/software/matita/contribs/assembly/freescale/memory_trees.ma similarity index 100% rename from helm/software/matita/library/freescale/memory_trees.ma rename to helm/software/matita/contribs/assembly/freescale/memory_trees.ma diff --git a/helm/software/matita/library/freescale/micro_tests.ma b/helm/software/matita/contribs/assembly/freescale/micro_tests.ma similarity index 100% rename from helm/software/matita/library/freescale/micro_tests.ma rename to helm/software/matita/contribs/assembly/freescale/micro_tests.ma diff --git a/helm/software/matita/library/freescale/model.ma b/helm/software/matita/contribs/assembly/freescale/model.ma similarity index 100% rename from helm/software/matita/library/freescale/model.ma rename to helm/software/matita/contribs/assembly/freescale/model.ma diff --git a/helm/software/matita/library/freescale/multivm.ma b/helm/software/matita/contribs/assembly/freescale/multivm.ma similarity index 100% rename from helm/software/matita/library/freescale/multivm.ma rename to helm/software/matita/contribs/assembly/freescale/multivm.ma diff --git a/helm/software/matita/library/freescale/opcode.ma b/helm/software/matita/contribs/assembly/freescale/opcode.ma similarity index 100% rename from helm/software/matita/library/freescale/opcode.ma rename to helm/software/matita/contribs/assembly/freescale/opcode.ma diff --git a/helm/software/matita/library/freescale/status.ma b/helm/software/matita/contribs/assembly/freescale/status.ma similarity index 100% rename from helm/software/matita/library/freescale/status.ma rename to helm/software/matita/contribs/assembly/freescale/status.ma diff --git a/helm/software/matita/library/freescale/table_HC05.ma b/helm/software/matita/contribs/assembly/freescale/table_HC05.ma similarity index 100% rename from helm/software/matita/library/freescale/table_HC05.ma rename to helm/software/matita/contribs/assembly/freescale/table_HC05.ma diff --git a/helm/software/matita/library/freescale/table_HC05_tests.ma b/helm/software/matita/contribs/assembly/freescale/table_HC05_tests.ma similarity index 100% rename from helm/software/matita/library/freescale/table_HC05_tests.ma rename to helm/software/matita/contribs/assembly/freescale/table_HC05_tests.ma diff --git a/helm/software/matita/library/freescale/table_HC08.ma b/helm/software/matita/contribs/assembly/freescale/table_HC08.ma similarity index 100% rename from helm/software/matita/library/freescale/table_HC08.ma rename to helm/software/matita/contribs/assembly/freescale/table_HC08.ma diff --git a/helm/software/matita/library/freescale/table_HC08_tests.ma b/helm/software/matita/contribs/assembly/freescale/table_HC08_tests.ma similarity index 100% rename from helm/software/matita/library/freescale/table_HC08_tests.ma rename to helm/software/matita/contribs/assembly/freescale/table_HC08_tests.ma diff --git a/helm/software/matita/library/freescale/table_HCS08.ma b/helm/software/matita/contribs/assembly/freescale/table_HCS08.ma similarity index 100% rename from helm/software/matita/library/freescale/table_HCS08.ma rename to helm/software/matita/contribs/assembly/freescale/table_HCS08.ma diff --git a/helm/software/matita/library/freescale/table_HCS08_tests.ma b/helm/software/matita/contribs/assembly/freescale/table_HCS08_tests.ma similarity index 100% rename from helm/software/matita/library/freescale/table_HCS08_tests.ma rename to helm/software/matita/contribs/assembly/freescale/table_HCS08_tests.ma diff --git a/helm/software/matita/library/freescale/table_RS08.ma b/helm/software/matita/contribs/assembly/freescale/table_RS08.ma similarity index 100% rename from helm/software/matita/library/freescale/table_RS08.ma rename to helm/software/matita/contribs/assembly/freescale/table_RS08.ma diff --git a/helm/software/matita/library/freescale/table_RS08_tests.ma b/helm/software/matita/contribs/assembly/freescale/table_RS08_tests.ma similarity index 100% rename from helm/software/matita/library/freescale/table_RS08_tests.ma rename to helm/software/matita/contribs/assembly/freescale/table_RS08_tests.ma diff --git a/helm/software/matita/library/freescale/tests.old b/helm/software/matita/contribs/assembly/freescale/tests.old similarity index 100% rename from helm/software/matita/library/freescale/tests.old rename to helm/software/matita/contribs/assembly/freescale/tests.old diff --git a/helm/software/matita/library/freescale/translation.ma b/helm/software/matita/contribs/assembly/freescale/translation.ma similarity index 100% rename from helm/software/matita/library/freescale/translation.ma rename to helm/software/matita/contribs/assembly/freescale/translation.ma diff --git a/helm/software/matita/library/freescale/word16.ma b/helm/software/matita/contribs/assembly/freescale/word16.ma similarity index 100% rename from helm/software/matita/library/freescale/word16.ma rename to helm/software/matita/contribs/assembly/freescale/word16.ma diff --git a/helm/software/matita/contribs/assembly/root b/helm/software/matita/contribs/assembly/root new file mode 100644 index 000000000..e6f78ade0 --- /dev/null +++ b/helm/software/matita/contribs/assembly/root @@ -0,0 +1 @@ +baseuri=cic:/matita diff --git a/helm/software/matita/library/depends b/helm/software/matita/library/depends index e02dc916f..a10d64a30 100644 --- a/helm/software/matita/library/depends +++ b/helm/software/matita/library/depends @@ -1,116 +1,88 @@ -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 +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 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 -Z/dirichlet_product.ma Z/sigma_p.ma Z/times.ma nat/primes.ma -Z/z.ma datatypes/bool.ma nat/nat.ma -Z/inversion.ma Z/dirichlet_product.ma Z/moebius.ma -Z/orders.ma Z/z.ma logic/connectives.ma nat/orders.ma Z/sigma_p.ma Z/plus.ma Z/times.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma -Z/times.ma Z/plus.ma nat/lt_arith.ma -decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma -decidable_kit/fgraph.ma decidable_kit/fintype.ma -decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma -decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma -decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma -decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma -higher_order_defs/functions.ma logic/equality.ma -higher_order_defs/ordering.ma logic/equality.ma -higher_order_defs/relations.ma logic/connectives.ma -Q/q.ma Z/compare.ma Z/plus.ma -Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma -Fsub/part1a_inversion.ma Fsub/defn.ma -Fsub/part1a.ma Fsub/defn.ma -Fsub/defn.ma Fsub/util.ma -Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma -datatypes/compare.ma +Z/z.ma datatypes/bool.ma nat/nat.ma datatypes/constructors.ma logic/equality.ma +datatypes/compare.ma datatypes/bool.ma higher_order_defs/functions.ma logic/equality.ma -algebra/monoids.ma algebra/semigroups.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/groups.ma algebra/monoids.ma datatypes/bool.ma logic/connectives.ma nat/compare.ma nat/le_arith.ma -algebra/CoRN/Setoids.ma Z/plus.ma datatypes/constructors.ma higher_order_defs/relations.ma logic/equality.ma nat/nat.ma +algebra/monoids.ma algebra/semigroups.ma +algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma 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 -algebra/CoRN/SetoidInc.ma algebra/CoRN/SetoidFun.ma -logic/coimplication.ma logic/connectives.ma +demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma +demo/realisability.ma datatypes/constructors.ma logic/connectives.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 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 -freescale/memory_func.ma freescale/memory_struct.ma -freescale/extra.ma datatypes/constructors.ma list/list.ma logic/connectives.ma nat/div_and_mod.ma nat/primes.ma -freescale/status.ma freescale/memory_abs.ma -freescale/memory_bits.ma freescale/memory_trees.ma -freescale/load_write.ma freescale/model.ma -freescale/micro_tests.ma freescale/multivm.ma -freescale/byte8.ma freescale/exadecim.ma -freescale/table_HCS08.ma freescale/opcode.ma -freescale/multivm.ma freescale/load_write.ma -freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma -freescale/translation.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma -freescale/model.ma freescale/status.ma -freescale/medium_tests.ma freescale/medium_tests_lemmas.ma -freescale/table_RS08.ma freescale/opcode.ma -freescale/table_HC05.ma freescale/opcode.ma -freescale/opcode.ma freescale/aux_bases.ma -freescale/table_HC08.ma freescale/opcode.ma -freescale/memory_trees.ma freescale/memory_struct.ma -freescale/aux_bases.ma freescale/word16.ma -freescale/memory_struct.ma freescale/translation.ma -freescale/exadecim.ma freescale/extra.ma -freescale/medium_tests_tools.ma freescale/multivm.ma -freescale/word16.ma freescale/byte8.ma -freescale/medium_tests_lemmas.ma freescale/medium_tests_tools.ma -freescale/table_HC05_tests.ma freescale/table_HC05.ma -freescale/table_RS08_tests.ma freescale/table_RS08.ma -freescale/table_HC08_tests.ma freescale/table_HC08.ma -freescale/table_HCS08_tests.ma freescale/table_HCS08.ma -technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma -demo/realisability.ma datatypes/constructors.ma logic/connectives.ma -demo/power_derivative.ma nat/compare.ma nat/nat.ma nat/orders.ma nat/plus.ma -demo/propositional_sequent_calculus.ma datatypes/constructors.ma list/sort.ma nat/compare.ma nat/plus.ma -nat/plus.ma nat/nat.ma -nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma -nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma +nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma +nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma nat/factorial2.ma nat/exp.ma nat/factorial.ma -nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma -nat/le_arith.ma nat/orders.ma nat/times.ma -nat/chebyshev_thm.ma nat/neper.ma +nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma nat/congruence.ma nat/primes.ma nat/relevant_equations.ma -nat/count.ma nat/permutation.ma nat/relevant_equations.ma nat/sigma_and_pi.ma -nat/div_and_mod_diseq.ma nat/lt_arith.ma -nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma -nat/gcd_properties1.ma nat/gcd.ma -nat/binomial.ma nat/factorial2.ma nat/iteration2.ma nat/minus.ma nat/compare.ma nat/le_arith.ma -nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma +nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma +nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma +nat/factorial.ma nat/le_arith.ma +nat/nth_prime.ma nat/lt_arith.ma nat/primes.ma +nat/binomial.ma nat/factorial2.ma nat/iteration2.ma nat/chebyshev_teta.ma nat/binomial.ma nat/pi_p.ma -nat/div_and_mod.ma datatypes/constructors.ma nat/minus.ma +nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/exp.ma nat/div_and_mod.ma nat/lt_arith.ma nat/minimization.ma nat/minus.ma -nat/relevant_equations.ma nat/gcd.ma nat/minus.ma nat/times.ma +nat/gcd.ma nat/lt_arith.ma nat/primes.ma +nat/chebyshev_thm.ma nat/neper.ma +nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma nat/sigma_and_pi.ma nat/exp.ma nat/factorial.ma nat/lt_arith.ma +nat/le_arith.ma nat/orders.ma nat/times.ma +nat/sqrt.ma nat/compare.ma nat/log.ma nat/times.ma +nat/times.ma nat/plus.ma +nat/div_and_mod_diseq.ma nat/lt_arith.ma nat/generic_iter_p.ma nat/div_and_mod_diseq.ma nat/ord.ma nat/primes.ma -nat/fermat_little_theorem.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma +nat/gcd_properties1.ma nat/gcd.ma +nat/totient.ma nat/chinese_reminder.ma nat/iteration2.ma +nat/lt_arith.ma nat/div_and_mod.ma +nat/bertrand.ma list/list.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma +nat/factorization.ma nat/ord.ma +nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma +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/nth_prime.ma nat/lt_arith.ma nat/primes.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 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/gcd.ma nat/lt_arith.ma nat/primes.ma -nat/o.ma nat/binomial.ma nat/sqrt.ma -nat/orders.ma logic/connectives.ma higher_order_defs/ordering.ma nat/nat.ma +nat/plus.ma nat/nat.ma nat/euler_theorem.ma nat/nat.ma nat/map_iter_p.ma nat/totient.ma +nat/compare.ma datatypes/bool.ma datatypes/compare.ma nat/orders.ma nat/primes.ma logic/connectives.ma nat/div_and_mod.ma nat/factorial.ma nat/minimization.ma nat/sigma_and_pi.ma -nat/bertrand.ma list/list.ma nat/chebyshev.ma nat/chebyshev_teta.ma nat/o.ma nat/sqrt.ma -nat/chinese_reminder.ma nat/congruence.ma nat/exp.ma nat/gcd.ma nat/permutation.ma -nat/factorial.ma nat/le_arith.ma -nat/lt_arith.ma nat/div_and_mod.ma -nat/permutation.ma nat/compare.ma nat/sigma_and_pi.ma -nat/totient1.ma nat/compare.ma nat/gcd_properties1.ma nat/iteration2.ma nat/totient.ma -nat/neper.ma nat/binomial.ma nat/chebyshev.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/log.ma -nat/factorization.ma nat/ord.ma -nat/map_iter_p.ma nat/count.ma nat/permutation.ma -nat/iteration2.ma nat/count.ma nat/generic_iter_p.ma nat/ord.ma nat/primes.ma -nat/chebyshev.ma nat/factorial2.ma nat/factorization.ma nat/log.ma nat/pi_p.ma -nat/log.ma datatypes/constructors.ma nat/div_and_mod_diseq.ma nat/iteration2.ma nat/minimization.ma nat/primes.ma nat/relevant_equations.ma -nat/times.ma nat/plus.ma +nat/ord.ma datatypes/constructors.ma nat/exp.ma nat/gcd.ma nat/nth_prime.ma nat/relevant_equations.ma +nat/o.ma nat/binomial.ma nat/sqrt.ma +Q/Qaxioms.ma Z/compare.ma Z/times.ma nat/iteration2.ma +Q/q.ma Z/compare.ma Z/plus.ma +technicalities/setoids.ma datatypes/constructors.ma logic/coimplication.ma logic/connectives2.ma +Fsub/part1a.ma Fsub/defn.ma +Fsub/util.ma list/list.ma logic/equality.ma nat/compare.ma +Fsub/defn.ma Fsub/util.ma +Fsub/part1a_inversion.ma Fsub/defn.ma +decidable_kit/streicher.ma logic/connectives.ma logic/equality.ma +decidable_kit/decidable.ma datatypes/bool.ma decidable_kit/streicher.ma logic/connectives.ma nat/compare.ma +decidable_kit/fgraph.ma decidable_kit/fintype.ma +decidable_kit/eqtype.ma datatypes/constructors.ma decidable_kit/decidable.ma +decidable_kit/list_aux.ma decidable_kit/eqtype.ma list/list.ma nat/plus.ma +decidable_kit/fintype.ma decidable_kit/eqtype.ma decidable_kit/list_aux.ma +higher_order_defs/relations.ma logic/connectives.ma +higher_order_defs/functions.ma logic/equality.ma +higher_order_defs/ordering.ma logic/equality.ma -- 2.39.2