]> matita.cs.unibo.it Git - helm.git/commit
- commit of the "reduction" component with two additions ...
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 18 Jan 2014 22:05:09 +0000 (22:05 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 18 Jan 2014 22:05:09 +0000 (22:05 +0000)
commit2ba2dc23443ad764adab652e06d6f5ed10bd912d
treed99279aa55a0accc2a8cd067b85c140126d6d360
parent3d953276edded0659cc73489290da43fb3ebb94c
- commit of the "reduction" component with two additions ...
- formal bug fix in extended substitution under a binder: now we
follow the paradigm used for reduction under a binder
28 files changed:
matita/matita/contribs/lambdadelta/basic_2/reduction/cir.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cir_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cix.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cix_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cnx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma [new file with mode: 0644]
matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crr_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crx.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/crx_lift.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl