From eb918fc784eacd2094e3986ba321ef47690d9983 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 10 Mar 2012 14:46:11 +0000 Subject: [PATCH 1/1] We are decapitalizing the contributions' names ... --- matita/matita/contribs/lambda_delta/Makefile | 87 ++++++++++--------- .../{Apps_2 => apps_2}/functional/lift.ma | 0 .../{Apps_2 => apps_2}/functional/notation.ma | 0 .../{Apps_2 => apps_2}/functional/rtm.ma | 0 .../{Apps_2 => apps_2}/functional/rtm_step.ma | 0 .../{Apps_2 => apps_2}/functional/subst.ma | 0 .../{Basic_2 => basic_2}/Basic_1.txt | 0 .../{Basic_2 => basic_2}/computation/acp.ma | 0 .../computation/acp_aaa.ma | 0 .../computation/acp_cr.ma | 0 .../{Basic_2 => basic_2}/computation/cprs.ma | 0 .../computation/cprs_cprs.ma | 0 .../computation/cprs_lcpr.ma | 0 .../computation/cprs_lcprs.ma | 0 .../computation/cprs_lift.ma | 0 .../computation/cprs_tstc.ma | 0 .../computation/cprs_tstc_vector.ma | 0 .../{Basic_2 => basic_2}/computation/csn.ma | 0 .../computation/csn_aaa.ma | 0 .../computation/csn_cpr.ma | 0 .../computation/csn_cprs.ma | 0 .../computation/csn_lcpr.ma | 0 .../computation/csn_lcpr_vector.ma | 0 .../computation/csn_lift.ma | 0 .../computation/csn_vector.ma | 0 .../{Basic_2 => basic_2}/computation/lcprs.ma | 0 .../computation/lcprs_cprs.ma | 0 .../computation/lcprs_lcprs.ma | 0 .../{Basic_2 => basic_2}/computation/lsubc.ma | 0 .../computation/lsubc_ldrop.ma | 0 .../computation/lsubc_ldrops.ma | 0 .../computation/lsubc_lsuba.ma | 0 .../{Basic_2 => basic_2}/conversion/cpc.ma | 0 .../conversion/cpc_cpc.ma | 0 .../{Basic_2 => basic_2}/equivalence/cpcs.ma | 0 .../{Basic_2 => basic_2}/grammar/aarity.ma | 0 .../{Basic_2 => basic_2}/grammar/cl_shift.ma | 0 .../{Basic_2 => basic_2}/grammar/cl_weight.ma | 0 .../{Basic_2 => basic_2}/grammar/genv.ma | 0 .../{Basic_2 => basic_2}/grammar/item.ma | 0 .../{Basic_2 => basic_2}/grammar/lenv.ma | 0 .../grammar/lenv_length.ma | 0 .../grammar/lenv_weight.ma | 0 .../{Basic_2 => basic_2}/grammar/lsubs.ma | 0 .../{Basic_2 => basic_2}/grammar/term.ma | 0 .../grammar/term_simple.ma | 0 .../grammar/term_vector.ma | 0 .../grammar/term_weight.ma | 0 .../{Basic_2 => basic_2}/grammar/tshf.ma | 0 .../{Basic_2 => basic_2}/grammar/tstc.ma | 0 .../{Basic_2 => basic_2}/grammar/tstc_tstc.ma | 0 .../grammar/tstc_vector.ma | 0 .../{Basic_2 => basic_2}/names.txt | 0 .../{Basic_2 => basic_2}/notation.ma | 0 .../{Basic_2 => basic_2}/reducibility/cnf.ma | 0 .../reducibility/cnf_lift.ma | 0 .../{Basic_2 => basic_2}/reducibility/cpr.ma | 0 .../reducibility/cpr_cpr.ma | 0 .../reducibility/cpr_lift.ma | 0 .../reducibility/cpr_ltpr.ma | 0 .../reducibility/cpr_ltpss.ma | 0 .../{Basic_2 => basic_2}/reducibility/lcpr.ma | 0 .../reducibility/lcpr_cpr.ma | 0 .../{Basic_2 => basic_2}/reducibility/ltpr.ma | 0 .../reducibility/ltpr_ldrop.ma | 0 .../reducibility/ltpr_tps.ma | 0 .../{Basic_2 => basic_2}/reducibility/tif.ma | 0 .../{Basic_2 => basic_2}/reducibility/tnf.ma | 0 .../reducibility/tnf_tif.ma | 0 .../{Basic_2 => basic_2}/reducibility/tpr.ma | 0 .../reducibility/tpr_lift.ma | 0 .../reducibility/tpr_tpr.ma | 0 .../reducibility/tpr_tpss.ma | 0 .../{Basic_2 => basic_2}/reducibility/trf.ma | 0 .../reducibility/twhnf.ma | 0 .../{Basic_2 => basic_2}/static/aaa.ma | 0 .../{Basic_2 => basic_2}/static/aaa_aaa.ma | 0 .../{Basic_2 => basic_2}/static/aaa_lift.ma | 0 .../{Basic_2 => basic_2}/static/aaa_lifts.ma | 0 .../{Basic_2 => basic_2}/static/lsuba.ma | 0 .../{Basic_2 => basic_2}/static/lsuba_aaa.ma | 0 .../static/lsuba_ldrop.ma | 0 .../static/lsuba_lsuba.ma | 0 .../{Basic_2 => basic_2}/static/sh.ma | 0 .../substitution/gdrop.ma | 0 .../substitution/gdrop_gdrop.ma | 0 .../substitution/ldrop.ma | 0 .../substitution/ldrop_ldrop.ma | 0 .../{Basic_2 => basic_2}/substitution/lift.ma | 0 .../substitution/lift_lift.ma | 0 .../substitution/lift_lift_vector.ma | 0 .../substitution/lift_vector.ma | 0 .../{Basic_2 => basic_2}/substitution/ltps.ma | 0 .../substitution/ltps_ldrop.ma | 0 .../substitution/ltps_tps.ma | 0 .../{Basic_2 => basic_2}/substitution/tps.ma | 0 .../substitution/tps_lift.ma | 0 .../substitution/tps_tps.ma | 0 .../{Basic_2 => basic_2}/unfold/delift.ma | 0 .../unfold/delift_lift.ma | 0 .../{Basic_2 => basic_2}/unfold/gr2.ma | 0 .../{Basic_2 => basic_2}/unfold/gr2_gr2.ma | 0 .../{Basic_2 => basic_2}/unfold/gr2_minus.ma | 0 .../{Basic_2 => basic_2}/unfold/gr2_plus.ma | 0 .../{Basic_2 => basic_2}/unfold/ldrops.ma | 0 .../unfold/ldrops_ldrop.ma | 0 .../unfold/ldrops_ldrops.ma | 0 .../{Basic_2 => basic_2}/unfold/lifts.ma | 0 .../{Basic_2 => basic_2}/unfold/lifts_lift.ma | 0 .../unfold/lifts_lift_vector.ma | 0 .../unfold/lifts_lifts.ma | 0 .../unfold/lifts_vector.ma | 0 .../{Basic_2 => basic_2}/unfold/ltpss.ma | 0 .../unfold/ltpss_ldrop.ma | 0 .../unfold/ltpss_ltpss.ma | 0 .../{Basic_2 => basic_2}/unfold/ltpss_tpss.ma | 0 .../{Basic_2 => basic_2}/unfold/tpss.ma | 0 .../{Basic_2 => basic_2}/unfold/tpss_lift.ma | 0 .../{Basic_2 => basic_2}/unfold/tpss_ltps.ma | 0 .../{Basic_2 => basic_2}/unfold/tpss_tpss.ma | 0 .../{Ground_2 => ground_2}/arith.ma | 0 .../{Ground_2 => ground_2}/list.ma | 0 .../{Ground_2 => ground_2}/notation.ma | 0 .../{Ground_2 => ground_2}/star.ma | 0 .../{Ground_2 => ground_2}/tri.ma | 0 .../{Ground_2 => ground_2}/xoa.conf.xml | 0 .../{Ground_2 => ground_2}/xoa.ma | 0 .../{Ground_2 => ground_2}/xoa_notation.ma | 0 .../{Ground_2 => ground_2}/xoa_props.ma | 0 129 files changed, 47 insertions(+), 40 deletions(-) rename matita/matita/contribs/lambda_delta/{Apps_2 => apps_2}/functional/lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Apps_2 => apps_2}/functional/notation.ma (100%) rename matita/matita/contribs/lambda_delta/{Apps_2 => apps_2}/functional/rtm.ma (100%) rename matita/matita/contribs/lambda_delta/{Apps_2 => apps_2}/functional/rtm_step.ma (100%) rename matita/matita/contribs/lambda_delta/{Apps_2 => apps_2}/functional/subst.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/Basic_1.txt (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/acp.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/acp_aaa.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/acp_cr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/cprs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/cprs_cprs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/cprs_lcpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/cprs_lcprs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/cprs_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/cprs_tstc.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/cprs_tstc_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn_aaa.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn_cpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn_cprs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn_lcpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn_lcpr_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/csn_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/lcprs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/lcprs_cprs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/lcprs_lcprs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/lsubc.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/lsubc_ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/lsubc_ldrops.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/computation/lsubc_lsuba.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/conversion/cpc.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/conversion/cpc_cpc.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/equivalence/cpcs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/aarity.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/cl_shift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/cl_weight.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/genv.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/item.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/lenv.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/lenv_length.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/lenv_weight.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/lsubs.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/term.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/term_simple.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/term_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/term_weight.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/tshf.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/tstc.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/tstc_tstc.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/grammar/tstc_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/names.txt (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/notation.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/cnf.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/cnf_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/cpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/cpr_cpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/cpr_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/cpr_ltpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/cpr_ltpss.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/lcpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/lcpr_cpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/ltpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/ltpr_ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/ltpr_tps.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/tif.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/tnf.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/tnf_tif.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/tpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/tpr_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/tpr_tpr.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/tpr_tpss.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/trf.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/reducibility/twhnf.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/aaa.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/aaa_aaa.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/aaa_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/aaa_lifts.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/lsuba.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/lsuba_aaa.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/lsuba_ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/lsuba_lsuba.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/static/sh.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/gdrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/gdrop_gdrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/ldrop_ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/lift_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/lift_lift_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/lift_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/ltps.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/ltps_ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/ltps_tps.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/tps.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/tps_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/substitution/tps_tps.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/delift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/delift_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/gr2.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/gr2_gr2.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/gr2_minus.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/gr2_plus.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/ldrops.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/ldrops_ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/ldrops_ldrops.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/lifts.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/lifts_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/lifts_lift_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/lifts_lifts.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/lifts_vector.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/ltpss.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/ltpss_ldrop.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/ltpss_ltpss.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/ltpss_tpss.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/tpss.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/tpss_lift.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/tpss_ltps.ma (100%) rename matita/matita/contribs/lambda_delta/{Basic_2 => basic_2}/unfold/tpss_tpss.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/arith.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/list.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/notation.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/star.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/tri.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/xoa.conf.xml (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/xoa.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/xoa_notation.ma (100%) rename matita/matita/contribs/lambda_delta/{Ground_2 => ground_2}/xoa_props.ma (100%) diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile index 5d86a4dd2..49e7e1b23 100644 --- a/matita/matita/contribs/lambda_delta/Makefile +++ b/matita/matita/contribs/lambda_delta/Makefile @@ -59,43 +59,50 @@ stats: $(PACKAGES:%=%.stats) @printf ' %-10s' '' @printf '\x1B[0m\n' -# sum ######################################################################## - -tbls: $(PACKAGES:%=etc/ld_%_sum.tbl) - -etc/ld_%_sum.tbl: MAS = $(shell find $* -name "*.ma") - -%.tbl: V1 = $(shell ls $(MAS) | wc -l) -%.tbl: C1 = $(shell grep "inductive \|record " $(MAS) | wc -l) -%.tbl: C2 = $(shell grep "definition \|let rec " $(MAS) | wc -l) -%.tbl: C3 = $(shell grep "inductive \|record \|definition \|let rec " $(MAS) | wc -l) -%.tbl: P1 = $(shell grep "theorem " $(MAS) | wc -l) -%.tbl: P2 = $(shell grep "lemma " $(MAS) | wc -l) -%.tbl: P3 = $(shell grep "lemma \|theorem " $(MAS) | wc -l) - -etc/ld_%_sum.tbl: $(MAS) - @mkdir -p etc - @printf 'Summary for: $*\n' - @printf 'name "$(basename $(@F))"\n\n' > $@ - @printf 'table {\n' >> $@ - @printf ' class "grey" [ "category"\n' >> $@ - @printf ' [ "objects" * ]\n' >> $@ - @printf ' ]\n' >> $@ - @printf ' class "cyan" [ "volume"\n' >> $@ - @printf ' [ "files" "$(V1)" * ]\n' >> $@ - @printf ' [ 4 ]\n' >> $@ - @printf ' ]\n' >> $@ - @printf ' class "green" [ "propositions"\n' >> $@ - @printf ' [ "theorems" "$(P1)" * ]\n' >> $@ - @printf ' [ "lemmas" "$(P2)" * ]\n' >> $@ - @printf ' [ "total" "$(P3)" * ]\n' >> $@ - @printf ' ]\n' >> $@ - @printf ' class "yellow" [ "concepts"\n' >> $@ - @printf ' [ "declared" "$(C1)" * ]\n' >> $@ - @printf ' [ "defined" "$(C2)" * ]\n' >> $@ - @printf ' [ "total" "$(C3)" * ]\n' >> $@ - @printf ' ]\n' >> $@ - @printf '}\n\n' >> $@ - @printf 'class "component" { 0 }\n\n' >> $@ - @printf 'class "plane" { 1 } { 3 } { 5 }\n\n' >> $@ - @printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $@ +# summary #################################################################### + +define SUMMARY_TEMPLATE + TBL_$(1) := $(1)/ld_$(1)_sum.tbl + MAS_$(1) := $$(shell find $(1) -name "*.ma") + TBLS += $$(TBL_$(1)) + + $$(TBL_$(1)): V1 := $$(shell ls $$(MAS_$(1)) | wc -l) + $$(TBL_$(1)): V2 := $$(shell cat $$(MAS_$(1)) | wc -c) + $$(TBL_$(1)): C1 := $$(shell grep "inductive \|record " $$(MAS_$(1)) | wc -l) + $$(TBL_$(1)): C2 := $$(shell grep "definition \|let rec " $$(MAS_$(1)) | wc -l) + $$(TBL_$(1)): C3 := $$(shell grep "inductive \|record \|definition \|let rec " $$(MAS_$(1)) | wc -l) + $$(TBL_$(1)): P1 := $$(shell grep "theorem " $$(MAS_$(1)) | wc -l) + $$(TBL_$(1)): P2 := $$(shell grep "lemma " $$(MAS_$(1)) | wc -l) + $$(TBL_$(1)): P3 := $$(shell grep "lemma \|theorem " $$(MAS_$(1)) | wc -l) + + $$(TBL_$(1)): $$(MAS_$(1)) + @printf ' SUMMARY $(1)\n' + @printf 'name "$$(basename $$(@F))"\n\n' > $$@ + @printf 'table {\n' >> $$@ + @printf ' class "grey" [ "category"\n' >> $$@ + @printf ' [ "objects" * ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "cyan" [ "sizes"\n' >> $$@ + @printf ' [ "files" "$$(V1)" ]\n' >> $$@ + @printf ' [ "bytes" "$$(V2)" ]\n' >> $$@ + @printf ' [ * ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "green" [ "propositions"\n' >> $$@ + @printf ' [ "theorems" "$$(P1)" ]\n' >> $$@ + @printf ' [ "lemmas" "$$(P2)" ]\n' >> $$@ + @printf ' [ "total" "$$(P3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf ' class "yellow" [ "concepts"\n' >> $$@ + @printf ' [ "declared" "$$(C1)" ]\n' >> $$@ + @printf ' [ "defined" "$$(C2)" ]\n' >> $$@ + @printf ' [ "total" "$$(C3)" ]\n' >> $$@ + @printf ' ]\n' >> $$@ + @printf '}\n\n' >> $$@ + @printf 'class "component" { 0 }\n\n' >> $$@ + @printf 'class "plane" { 1 } { 3 } { 5 }\n\n' >> $$@ + @printf 'class "number" { 2 } { 4 } { 6 }\n\n' >> $$@ +endef + +$(foreach PKG, $(PACKAGES), $(eval $(call SUMMARY_TEMPLATE,$(PKG)))) + +tbls: $(TBLS) diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Apps_2/functional/lift.ma rename to matita/matita/contribs/lambda_delta/apps_2/functional/lift.ma diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Apps_2/functional/notation.ma rename to matita/matita/contribs/lambda_delta/apps_2/functional/notation.ma diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Apps_2/functional/rtm.ma rename to matita/matita/contribs/lambda_delta/apps_2/functional/rtm.ma diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Apps_2/functional/rtm_step.ma rename to matita/matita/contribs/lambda_delta/apps_2/functional/rtm_step.ma diff --git a/matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Apps_2/functional/subst.ma rename to matita/matita/contribs/lambda_delta/apps_2/functional/subst.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/Basic_1.txt similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt rename to matita/matita/contribs/lambda_delta/basic_2/Basic_1.txt diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/acp.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/acp_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/acp_cr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/cprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_cprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lcprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lcprs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/cprs_tstc_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/cprs_tstc_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_cprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lcpr_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_lcpr_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/csn_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lcprs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_cprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_cprs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_lcprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lcprs_lcprs.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lcprs_lcprs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lsubc.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrops.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_ldrops.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_lsuba.ma rename to matita/matita/contribs/lambda_delta/basic_2/computation/lsubc_lsuba.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc.ma rename to matita/matita/contribs/lambda_delta/basic_2/conversion/cpc.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/conversion/cpc_cpc.ma rename to matita/matita/contribs/lambda_delta/basic_2/conversion/cpc_cpc.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/equivalence/cpcs.ma b/matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/equivalence/cpcs.ma rename to matita/matita/contribs/lambda_delta/basic_2/equivalence/cpcs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/aarity.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/cl_shift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/cl_weight.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/genv.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/item.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_length.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_length.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv_weight.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lsubs.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/lsubs.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/term.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/term_simple.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/term_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/term_weight.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/term_weight.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/tshf.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/tshf.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/tstc.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_tstc.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_tstc.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_tstc.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/grammar/tstc_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/grammar/tstc_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/names.txt b/matita/matita/contribs/lambda_delta/basic_2/names.txt similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/names.txt rename to matita/matita/contribs/lambda_delta/basic_2/names.txt diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/notation.ma rename to matita/matita/contribs/lambda_delta/basic_2/notation.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cnf_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_ltpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr_ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/lcpr_cpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/lcpr_cpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr_tps.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/ltpr_tps.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tif.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/tif.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_tif.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf_tif.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/tnf_tif.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/trf.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/reducibility/twhnf.ma rename to matita/matita/contribs/lambda_delta/basic_2/reducibility/twhnf.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/aaa.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/aaa_aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/aaa_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/aaa_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/aaa_lifts.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/aaa_lifts.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/lsuba.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_aaa.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_aaa.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/lsuba_aaa.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/lsuba_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_lsuba.ma b/matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/lsuba_lsuba.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/lsuba_lsuba.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sh.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/static/sh.ma rename to matita/matita/contribs/lambda_delta/basic_2/static/sh.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop_gdrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/gdrop_gdrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_lift_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/lift_lift_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/lift_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/lift_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/ltps.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/ltps_tps.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/tps_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma rename to matita/matita/contribs/lambda_delta/basic_2/substitution/tps_tps.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/delift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/delift_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/gr2.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_gr2.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_gr2.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_minus.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_minus.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/gr2_plus.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/gr2_plus.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrops.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops_ldrops.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ldrops_ldrops.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/lifts.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lift_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lift_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_lifts.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_lifts.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ltpss.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_lift.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_ltps.ma diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_tpss.ma rename to matita/matita/contribs/lambda_delta/basic_2/unfold/tpss_tpss.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/ground_2/arith.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/arith.ma rename to matita/matita/contribs/lambda_delta/ground_2/arith.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/list.ma b/matita/matita/contribs/lambda_delta/ground_2/list.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/list.ma rename to matita/matita/contribs/lambda_delta/ground_2/list.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/notation.ma b/matita/matita/contribs/lambda_delta/ground_2/notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/notation.ma rename to matita/matita/contribs/lambda_delta/ground_2/notation.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/star.ma rename to matita/matita/contribs/lambda_delta/ground_2/star.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/tri.ma b/matita/matita/contribs/lambda_delta/ground_2/tri.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/tri.ma rename to matita/matita/contribs/lambda_delta/ground_2/tri.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml rename to matita/matita/contribs/lambda_delta/ground_2/xoa.conf.xml diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/xoa.ma rename to matita/matita/contribs/lambda_delta/ground_2/xoa.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma rename to matita/matita/contribs/lambda_delta/ground_2/xoa_notation.ma diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma similarity index 100% rename from matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma rename to matita/matita/contribs/lambda_delta/ground_2/xoa_props.ma -- 2.39.2