]> matita.cs.unibo.it Git - helm.git/commit
- procedural: bugfix in "Barendregt convention" test
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Apr 2009 20:58:49 +0000 (20:58 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Wed, 29 Apr 2009 20:58:49 +0000 (20:58 +0000)
commit1e1f24496beba354fb3f550496858b5755d9be0b
tree955b88a05afe1d231e6d8727d44a06b9b689414d
parent820e0ea35f999236e0a55915c1d40cf745ffd6b9
- procedural: bugfix in "Barendregt convention" test
- library/logic/cprop_connectives.ma: reorganized.
notations must immediately follow the definition they refer to (or else another
definition can use them in the reconstructed version of the file)
- core_notation.moo: added a notation for non-functiona 'exists
eta-expansion (not a CIC conversion) should be avoided exp. if the rendered
text must be reparsed (ie. during the reconstruction)
"default" notation facility reactivated in parsing mode since it is not
equivalent to the separated rules (they cover eachother).
The bug is in the rendering mode
- applyTransformation: debugging information added (commented)

logic/cprop_connectives.ma reconstructed and compiled !!
helm/software/components/acic_procedural/procedural2.ml
helm/software/components/acic_procedural/proceduralHelpers.ml
helm/software/components/acic_procedural/proceduralHelpers.mli
helm/software/components/acic_procedural/proceduralOptimizer.ml
helm/software/components/syntax_extensions/.depend
helm/software/matita/applyTransformation.ml
helm/software/matita/core_notation.moo
helm/software/matita/library/logic/connectives.ma
helm/software/matita/library/logic/cprop_connectives.ma