From: Ferruccio Guidi Date: Sun, 29 Jun 2014 20:24:42 +0000 (+0000) Subject: - wrong version of drop was used in four places X-Git-Tag: make_still_working~889 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=645b62762e9c86e343d4741541a2ddccfed8ebc7 - wrong version of drop was used in four places - bugfixed css class in tables --- diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index 10b7261cf..2945fc62c 100644 --- a/matita/matita/contribs/lambdadelta/Makefile +++ b/matita/matita/contribs/lambdadelta/Makefile @@ -30,7 +30,9 @@ PRB_OPTS := $(XOA_OPTS) -g ORIG := . ./orig.sh ORIGS := basic_2/basic_1.orig -TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim +CONTRIB := lambdadelta_2 + +TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib PACKAGES := ground_2 basic_2 apps_2 @@ -191,7 +193,7 @@ define SUMMARY_TEMPLATE @printf ' SUMMARY $(1)\n' @printf 'name "$$(basename $$(@F))"\n\n' > $$@ @printf 'table {\n' >> $$@ - @printf ' class "grey" [ "category"\n' >> $$@ + @printf ' class "gray" [ "category"\n' >> $$@ @printf ' [ "objects" * ]\n' >> $$@ @printf ' ]\n' >> $$@ @printf ' class "cyan" [ "sizes"\n' >> $$@ @@ -233,6 +235,12 @@ TRIMS := $(MAS) $(TBLS) $(LDWS) trim: $(TRIMS:%=%.trimmed) +# contrib #################################################################### + +contrib: + @echo " TAR -czf $(CONTRIB).tar.gz root *.ma" + $(H)tar -czf $(CONTRIB).tar.gz root $(MAS) + ############################################################################## .PHONY: $(TAGS) diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl index 3bd24d90e..f854d14ea 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl @@ -1,7 +1,7 @@ name "apps_2_src" table { - class "grey" + class "gray" [ { "component" * } { [ { "plane" * } { [ "files" * ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma index 08d284d97..425a7f82a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma @@ -145,11 +145,11 @@ elim (cpxs_inv_appl1 … H) -H * @(cpxs_trans … HU) -U elim (cpxs_inv_abbr1 … HT0) -HT0 * [ #V1 #T1 #HV1 #HT1 #H destruct - lapply (cpxs_lift … HV10a (L.ⓓV) (Ⓣ) … HV12a … HV0a) -V1a -V0a [ /2 width=1 by drop_drop/ ] #HV2a + lapply (cpxs_lift … HV10a (L.ⓓV) (Ⓕ) … HV12a … HV0a) -V1a -V0a [ /2 width=1 by drop_drop/ ] #HV2a @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/ | #X #HT1 #H #H0 destruct elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct - lapply (cpxs_lift … HV10a (L.ⓓV0) (Ⓣ) … HV12a … HV0a) -V0a [ /2 width=1 by drop_drop/ ] #HV2a + lapply (cpxs_lift … HV10a (L.ⓓV0) (Ⓕ) … HV12a … HV0a) -V0a [ /2 width=1 by drop_drop/ ] #HV2a @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1 @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma index f3f78ccb5..80755fc0b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lpx.ma @@ -96,12 +96,12 @@ elim (cpx_inv_appl1 … HL) -HL * | * #_ #H elim H // ] | -H -HVT #H - lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓣ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by drop_drop/ #HV24 + lapply (cpx_lift … HLV10 (L.ⓓV) (Ⓕ) … HV12 … HV04) -HLV10 -HV12 /2 width=1 by drop_drop/ #HV24 @(IHVT … H … HV04) -IHVT /4 width=1 by cpx_cpxs, cpx_bind, cpx_flat/ ] | -H -IHVT #T0 #HLT0 #HT0 #H0 destruct lapply (csx_cpx_trans … HVT (ⓐV2.T0) ?) /2 width=1 by cpx_flat/ -T #HVT0 - lapply (csx_inv_lift … L … (Ⓣ) … 1 HVT0 ? ? ?) -HVT0 + lapply (csx_inv_lift … L … (Ⓕ) … 1 HVT0 ? ? ?) -HVT0 /3 width=5 by csx_cpx_trans, cpx_pair_sn, drop_drop, lift_flat/ ] | -HV -HV12 -HVT -IHVT -H #b #V0 #W0 #W1 #T0 #T1 #_ #_ #_ #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl index 0de7f19e6..7d5f0649b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_blk.tbl @@ -1,7 +1,7 @@ name "basic_2_blk" table { - class "grey" [ { "domain" * } { + class "gray" [ { "domain" * } { [ [ "block" ] [ "leader" ] [ "applicator (with →θ)*" ] [ "reduction" ] [ "→ζ *" ] [ "reference *" ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index c2eecbacd..880a674aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -1,7 +1,7 @@ name "basic_2_src" table { - class "grey" + class "gray" [ { "component" * } { [ { "plane" * } { [ "files" * ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 9f5153f50..c5e65b0b5 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -1,7 +1,7 @@ name "ground_2_src" table { - class "grey" + class "gray" [ { "plane" * } { [ "files" * ] }