]> matita.cs.unibo.it Git - helm.git/commit
- exclusion binder added in local environments
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 16 Oct 2017 21:34:59 +0000 (21:34 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 16 Oct 2017 21:34:59 +0000 (21:34 +0000)
commit98fbba1b68d457807c73ebf70eb2a48696381da4
tree47d1fdffefe669d8584582888d8f0f67570acead
parent65e6209e0758832835ba8d14304a1548d059a634
- exclusion binder added in local environments
  working components: syntax, relocation, s_transition, s_computation, static
- improved lsubf of which we hope to prove transitivity
- improvements in rtmap
86 files changed:
matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
matita/matita/contribs/lambdadelta/basic_2/etc/lsubf.etc [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ceq.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ext2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_length.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_bind.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_drops.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqup_weight.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus_drops.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/s_computation/fqus_weight.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_length.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_weight.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fquq.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fquq_length.ma
matita/matita/contribs/lambdadelta/basic_2/s_transition/fquq_weight.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/static/aaa_lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/static/frees_frees.ma
matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqus.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma
matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsuba.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsuba.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsuba_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubc.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubc_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsuba.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubc_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubf.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubf_lsubr.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_drops.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_length.ma
matita/matita/contribs/lambdadelta/basic_2/static/lsubr_lsubr.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/append.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/append_length.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/bind_ext2.ma [deleted file]
matita/matita/contribs/lambdadelta/basic_2/syntax/cl_restricted_weight.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/cl_weight.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/ext2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/syntax/ext2_ext2.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/syntax/item.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/lenv.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_ext2.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_length.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/lenv_weight.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma