]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d063dde) | patch
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
tree7538a1a5cffddf0709fd67babf71772b842162fatree | snapshot
parentd063ddede0424eb1f47a4c9769eaefbb16d90700commit | diff
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 diff | blob | history
helm/software/matita/core_notation.moo diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.