]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 473819a) | patch
We reintroduce the distinction between binding and non-binding items.
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 6 Jun 2011 17:19:30 +0000 (17:19 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 6 Jun 2011 17:19:30 +0000 (17:19 +0000)
commit7345613effa9d152f940b2ac637e9584c59c0d6e
tree011da4b7b14369f6b69e59a6adc82ee7ccf4c570tree | snapshot
parent473819a43c9f376324865ecb3b4534f4e6cc6248commit | diff
We reintroduce the distinction between binding and non-binding items.
Mon-binding items are now forbidden in environments
matita/matita/lib/lambda-delta/language/item.ma diff | blob | history
matita/matita/lib/lambda-delta/language/lenv.ma diff | blob | history
matita/matita/lib/lambda-delta/language/term.ma diff | blob | history
matita/matita/lib/lambda-delta/language/weight.ma diff | blob | history
matita/matita/lib/lambda-delta/notation.ma diff | blob | history
matita/matita/lib/lambda-delta/substitution/lift.ma diff | blob | history
matita/matita/lib/lambda-delta/substitution/subst.ma diff | blob | history
matita/matita/lib/lambda-delta/substitution/thin.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.