From bbb9215a02e1321d01a11c0ead6d0d218d047f68 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 22 Mar 2008 11:19:05 +0000 Subject: [PATCH] library_auto moved inside contrib, still not ported to the relatively-new build system --- helm/software/matita/contribs/Makefile | 2 +- helm/software/matita/{ => contribs}/library_auto/auto/Q/q.ma | 0 .../matita/{ => contribs}/library_auto/auto/Z/compare.ma | 0 .../matita/{ => contribs}/library_auto/auto/Z/orders.ma | 0 helm/software/matita/{ => contribs}/library_auto/auto/Z/plus.ma | 0 .../software/matita/{ => contribs}/library_auto/auto/Z/times.ma | 0 helm/software/matita/{ => contribs}/library_auto/auto/Z/z.ma | 0 .../{ => contribs}/library_auto/auto/nat/chinese_reminder.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/compare.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/congruence.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/count.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/div_and_mod.ma | 0 .../{ => contribs}/library_auto/auto/nat/euler_theorem.ma | 0 .../software/matita/{ => contribs}/library_auto/auto/nat/exp.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/factorial.ma | 0 .../{ => contribs}/library_auto/auto/nat/factorization.ma | 0 .../library_auto/auto/nat/fermat_little_theorem.ma | 0 .../software/matita/{ => contribs}/library_auto/auto/nat/gcd.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/le_arith.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/lt_arith.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/map_iter_p.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/minimization.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/minus.ma | 0 .../software/matita/{ => contribs}/library_auto/auto/nat/nat.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/nth_prime.ma | 0 .../software/matita/{ => contribs}/library_auto/auto/nat/ord.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/orders.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/permutation.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/plus.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/primes.ma | 0 .../{ => contribs}/library_auto/auto/nat/relevant_equations.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/sigma_and_pi.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/times.ma | 0 .../matita/{ => contribs}/library_auto/auto/nat/totient.ma | 0 helm/software/matita/{ => contribs}/library_auto/makefile | 0 35 files changed, 1 insertion(+), 1 deletion(-) rename helm/software/matita/{ => contribs}/library_auto/auto/Q/q.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/Z/compare.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/Z/orders.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/Z/plus.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/Z/times.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/Z/z.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/chinese_reminder.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/compare.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/congruence.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/count.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/div_and_mod.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/euler_theorem.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/exp.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/factorial.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/factorization.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/fermat_little_theorem.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/gcd.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/le_arith.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/lt_arith.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/map_iter_p.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/minimization.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/minus.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/nat.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/nth_prime.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/ord.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/orders.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/permutation.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/plus.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/primes.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/relevant_equations.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/sigma_and_pi.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/times.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/auto/nat/totient.ma (100%) rename helm/software/matita/{ => contribs}/library_auto/makefile (100%) diff --git a/helm/software/matita/contribs/Makefile b/helm/software/matita/contribs/Makefile index 97eb363c9..1ee722ed5 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 assembly +DEVELS = RELATIONAL LOGIC LAMBDA-TYPES assembly dama $(GOALS): @$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) diff --git a/helm/software/matita/library_auto/auto/Q/q.ma b/helm/software/matita/contribs/library_auto/auto/Q/q.ma similarity index 100% rename from helm/software/matita/library_auto/auto/Q/q.ma rename to helm/software/matita/contribs/library_auto/auto/Q/q.ma diff --git a/helm/software/matita/library_auto/auto/Z/compare.ma b/helm/software/matita/contribs/library_auto/auto/Z/compare.ma similarity index 100% rename from helm/software/matita/library_auto/auto/Z/compare.ma rename to helm/software/matita/contribs/library_auto/auto/Z/compare.ma diff --git a/helm/software/matita/library_auto/auto/Z/orders.ma b/helm/software/matita/contribs/library_auto/auto/Z/orders.ma similarity index 100% rename from helm/software/matita/library_auto/auto/Z/orders.ma rename to helm/software/matita/contribs/library_auto/auto/Z/orders.ma diff --git a/helm/software/matita/library_auto/auto/Z/plus.ma b/helm/software/matita/contribs/library_auto/auto/Z/plus.ma similarity index 100% rename from helm/software/matita/library_auto/auto/Z/plus.ma rename to helm/software/matita/contribs/library_auto/auto/Z/plus.ma diff --git a/helm/software/matita/library_auto/auto/Z/times.ma b/helm/software/matita/contribs/library_auto/auto/Z/times.ma similarity index 100% rename from helm/software/matita/library_auto/auto/Z/times.ma rename to helm/software/matita/contribs/library_auto/auto/Z/times.ma diff --git a/helm/software/matita/library_auto/auto/Z/z.ma b/helm/software/matita/contribs/library_auto/auto/Z/z.ma similarity index 100% rename from helm/software/matita/library_auto/auto/Z/z.ma rename to helm/software/matita/contribs/library_auto/auto/Z/z.ma diff --git a/helm/software/matita/library_auto/auto/nat/chinese_reminder.ma b/helm/software/matita/contribs/library_auto/auto/nat/chinese_reminder.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/chinese_reminder.ma rename to helm/software/matita/contribs/library_auto/auto/nat/chinese_reminder.ma diff --git a/helm/software/matita/library_auto/auto/nat/compare.ma b/helm/software/matita/contribs/library_auto/auto/nat/compare.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/compare.ma rename to helm/software/matita/contribs/library_auto/auto/nat/compare.ma diff --git a/helm/software/matita/library_auto/auto/nat/congruence.ma b/helm/software/matita/contribs/library_auto/auto/nat/congruence.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/congruence.ma rename to helm/software/matita/contribs/library_auto/auto/nat/congruence.ma diff --git a/helm/software/matita/library_auto/auto/nat/count.ma b/helm/software/matita/contribs/library_auto/auto/nat/count.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/count.ma rename to helm/software/matita/contribs/library_auto/auto/nat/count.ma diff --git a/helm/software/matita/library_auto/auto/nat/div_and_mod.ma b/helm/software/matita/contribs/library_auto/auto/nat/div_and_mod.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/div_and_mod.ma rename to helm/software/matita/contribs/library_auto/auto/nat/div_and_mod.ma diff --git a/helm/software/matita/library_auto/auto/nat/euler_theorem.ma b/helm/software/matita/contribs/library_auto/auto/nat/euler_theorem.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/euler_theorem.ma rename to helm/software/matita/contribs/library_auto/auto/nat/euler_theorem.ma diff --git a/helm/software/matita/library_auto/auto/nat/exp.ma b/helm/software/matita/contribs/library_auto/auto/nat/exp.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/exp.ma rename to helm/software/matita/contribs/library_auto/auto/nat/exp.ma diff --git a/helm/software/matita/library_auto/auto/nat/factorial.ma b/helm/software/matita/contribs/library_auto/auto/nat/factorial.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/factorial.ma rename to helm/software/matita/contribs/library_auto/auto/nat/factorial.ma diff --git a/helm/software/matita/library_auto/auto/nat/factorization.ma b/helm/software/matita/contribs/library_auto/auto/nat/factorization.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/factorization.ma rename to helm/software/matita/contribs/library_auto/auto/nat/factorization.ma diff --git a/helm/software/matita/library_auto/auto/nat/fermat_little_theorem.ma b/helm/software/matita/contribs/library_auto/auto/nat/fermat_little_theorem.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/fermat_little_theorem.ma rename to helm/software/matita/contribs/library_auto/auto/nat/fermat_little_theorem.ma diff --git a/helm/software/matita/library_auto/auto/nat/gcd.ma b/helm/software/matita/contribs/library_auto/auto/nat/gcd.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/gcd.ma rename to helm/software/matita/contribs/library_auto/auto/nat/gcd.ma diff --git a/helm/software/matita/library_auto/auto/nat/le_arith.ma b/helm/software/matita/contribs/library_auto/auto/nat/le_arith.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/le_arith.ma rename to helm/software/matita/contribs/library_auto/auto/nat/le_arith.ma diff --git a/helm/software/matita/library_auto/auto/nat/lt_arith.ma b/helm/software/matita/contribs/library_auto/auto/nat/lt_arith.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/lt_arith.ma rename to helm/software/matita/contribs/library_auto/auto/nat/lt_arith.ma diff --git a/helm/software/matita/library_auto/auto/nat/map_iter_p.ma b/helm/software/matita/contribs/library_auto/auto/nat/map_iter_p.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/map_iter_p.ma rename to helm/software/matita/contribs/library_auto/auto/nat/map_iter_p.ma diff --git a/helm/software/matita/library_auto/auto/nat/minimization.ma b/helm/software/matita/contribs/library_auto/auto/nat/minimization.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/minimization.ma rename to helm/software/matita/contribs/library_auto/auto/nat/minimization.ma diff --git a/helm/software/matita/library_auto/auto/nat/minus.ma b/helm/software/matita/contribs/library_auto/auto/nat/minus.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/minus.ma rename to helm/software/matita/contribs/library_auto/auto/nat/minus.ma diff --git a/helm/software/matita/library_auto/auto/nat/nat.ma b/helm/software/matita/contribs/library_auto/auto/nat/nat.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/nat.ma rename to helm/software/matita/contribs/library_auto/auto/nat/nat.ma diff --git a/helm/software/matita/library_auto/auto/nat/nth_prime.ma b/helm/software/matita/contribs/library_auto/auto/nat/nth_prime.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/nth_prime.ma rename to helm/software/matita/contribs/library_auto/auto/nat/nth_prime.ma diff --git a/helm/software/matita/library_auto/auto/nat/ord.ma b/helm/software/matita/contribs/library_auto/auto/nat/ord.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/ord.ma rename to helm/software/matita/contribs/library_auto/auto/nat/ord.ma diff --git a/helm/software/matita/library_auto/auto/nat/orders.ma b/helm/software/matita/contribs/library_auto/auto/nat/orders.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/orders.ma rename to helm/software/matita/contribs/library_auto/auto/nat/orders.ma diff --git a/helm/software/matita/library_auto/auto/nat/permutation.ma b/helm/software/matita/contribs/library_auto/auto/nat/permutation.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/permutation.ma rename to helm/software/matita/contribs/library_auto/auto/nat/permutation.ma diff --git a/helm/software/matita/library_auto/auto/nat/plus.ma b/helm/software/matita/contribs/library_auto/auto/nat/plus.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/plus.ma rename to helm/software/matita/contribs/library_auto/auto/nat/plus.ma diff --git a/helm/software/matita/library_auto/auto/nat/primes.ma b/helm/software/matita/contribs/library_auto/auto/nat/primes.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/primes.ma rename to helm/software/matita/contribs/library_auto/auto/nat/primes.ma diff --git a/helm/software/matita/library_auto/auto/nat/relevant_equations.ma b/helm/software/matita/contribs/library_auto/auto/nat/relevant_equations.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/relevant_equations.ma rename to helm/software/matita/contribs/library_auto/auto/nat/relevant_equations.ma diff --git a/helm/software/matita/library_auto/auto/nat/sigma_and_pi.ma b/helm/software/matita/contribs/library_auto/auto/nat/sigma_and_pi.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/sigma_and_pi.ma rename to helm/software/matita/contribs/library_auto/auto/nat/sigma_and_pi.ma diff --git a/helm/software/matita/library_auto/auto/nat/times.ma b/helm/software/matita/contribs/library_auto/auto/nat/times.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/times.ma rename to helm/software/matita/contribs/library_auto/auto/nat/times.ma diff --git a/helm/software/matita/library_auto/auto/nat/totient.ma b/helm/software/matita/contribs/library_auto/auto/nat/totient.ma similarity index 100% rename from helm/software/matita/library_auto/auto/nat/totient.ma rename to helm/software/matita/contribs/library_auto/auto/nat/totient.ma diff --git a/helm/software/matita/library_auto/makefile b/helm/software/matita/contribs/library_auto/makefile similarity index 100% rename from helm/software/matita/library_auto/makefile rename to helm/software/matita/contribs/library_auto/makefile -- 2.39.2