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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 15 Apr 2014 18:06:55 +0000 (18:06 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 15 Apr 2014 18:06:55 +0000 (18:06 +0000)
commit	07d915d411ffabeb0c7cd678f00cbeca53ae8276
tree	641e093df35b17f235669a7a4a34fd31d94a0544	tree \| snapshot
parent	c69a33bba2ae2f37953737940fb45149136cf054	commit \| diff

- lazy extended reduction parked
- fpns finally removed
- "big tree" computation based again on "full" extended reduction
but improved with lazy equivalence for local environments
- llor parked for now (something to fix there)

85 files changed:

matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_llpx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/csx_llpxs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbc.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbg_fpbg.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_ext.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_fpbs.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lift.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_lpr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_lleq.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_cpxs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_llpxs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llpxs_lprs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llsx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llsx_alt.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llsx_csx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llsx_ldrop.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/llsx_llpxs.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.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_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/cpxs_llpx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/csx_llpx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/csx_llpxs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/fpbs_lpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazypredsn_7.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazypredsnstar_7.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazysn_6.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/lazysnalt_6.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_aaa.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_lleq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpx_lpr.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_aaa.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_cpxs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_lleq.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_llpxs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llpxs_lprs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_alt.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_csx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_ldrop.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_llpx.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/llpx/llsx_llpxs.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/btpredsnstar_8.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbc_fpns.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbg_fpns.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbs_fpns.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpbu_fpns.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/fpns_fpns.etc	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq_llor.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llor.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_llor.etc	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsn_7.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazypredsnstar_7.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysn_6.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazysnalt_6.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/fpb_aaa.ma		diff \| blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_aaa.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lleq.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_lpr.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/relocation/llor.ma	[deleted file]	blob \| history
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lleq.ma	[new file with mode: 0644]	blob
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl		diff \| blob \| history

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

RSS Atom