]> matita.cs.unibo.it Git - helm.git/commit
Exists is no longer an ad-hoc notation hard-coded in the parser.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 11 Jul 2008 16:49:18 +0000 (16:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 11 Jul 2008 16:49:18 +0000 (16:49 +0000)
commit6f64f2bbba6d5488cc36b8e2f5a717e866a3015d
tree7538a1a5cffddf0709fd67babf71772b842162fa
parentd063ddede0424eb1f47a4c9769eaefbb16d90700
Exists is no longer an ad-hoc notation hard-coded in the parser.
It was so becauses it was previously impossible to declare a notation that
changed the level of its subterms.
helm/software/components/content_pres/cicNotationParser.ml
helm/software/matita/core_notation.moo