matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 4 Oct 2013 13:34:48 +0000 (13:34 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Fri, 4 Oct 2013 13:34:48 +0000 (13:34 +0000)
commit	fdb2c62b58006b82c015ba70b494d50c7860e28f
tree	13343d05cb27f341a97993776d2253790c88e8c8	tree \| snapshot
parent	4aa431513ffa0ce0accf81e6e9ea4b9314d468e3	commit \| diff

- degree assignment, static type assignment, iterated static type
assignment and lenv refinement for native validity reaxiomatized to
move lsubsv_snv_trans out of the mutual induction for preservation
- minor stylistic improvements and Makefile bugfix

119 files changed:

matita/matita/contribs/lambdadelta/Makefile		diff \| blob \| history
matita/matita/contribs/lambdadelta/apps_2/web/apps_2.ldw.xml		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpds.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpds_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpds_cpds.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpds_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_cpds.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsuba.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsubd.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_snv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_ssta.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_cpcs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_ssta_lpr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_sstas.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/ygt_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/ypr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/dynamic/yprs_yprs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/ysc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpes_cpds.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/sstas_ltpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/cpr/sta_ltpss.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/da/da.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/da/da_da.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/da/da_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/ssta/ssta.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/ssta/ssta_aaa.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/ssta/ssta_lift.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/ssta/ssta_ssta.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/ssta/statictype_7.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_aaa.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_lift.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_ltpss.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sstas/sstas_sstas.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_aaa.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_lift.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_ltpss.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sta/sta_sta.etc		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/sta/statictype_5.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/grammar/cl_shift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_append.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/names.txt		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/degree_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_6.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictype_7.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_7.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestaralt_7.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_crx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_lpx_sn.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/aaa_da.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/da.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/da_da.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/da_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/lsubd.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/lsubd_da.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/lsubd_lsubd.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/static/sd.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/ssta_ssta.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lifts_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_aaa.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lsstas.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/unfold/sstas.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_lift.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/sstas_sstas.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/star.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/xoa.conf.xml		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/xoa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/ground_2/xoa_notation.ma		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom