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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 20 Jul 2013 22:10:11 +0000 (22:10 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Sat, 20 Jul 2013 22:10:11 +0000 (22:10 +0000)
commit	f62eeb3c7824564ccbe4fff6e75ddee46ca39cc0
tree	e5035f127b10821c416d16db8f410c1ce8e56c71	tree \| snapshot
parent	ef49e0e7f5f298c299afdd3cbfdc2404ecb93879	commit \| diff

- new extendedd beta-reductum involving native type annotation
- extended strong normalization for simply typed terms (milestone)
- some renaming

50 files changed:

matita/matita/contribs/lambdadelta/basic_2/computation/acp.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/acp_cr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpe.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpe_cpe.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpre.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/cpre_cpre.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxe.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.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.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csn_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csn_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csn_lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csn_tstc_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csn_vector.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/dxprs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_ldrop.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lsubc_lsuba.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/equivalence/cpcs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/names.txt		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cix.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/reduction/lsubx_lsubx.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/substitution/cpss.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/substitution/lsubr_lsubr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/unfold/cpqs.ma		diff \| 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