]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 650e3b3) | patch
Partial bug fix: every inner type is now added to the selection roots.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 29 Jul 2005 09:00:32 +0000 (09:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 29 Jul 2005 09:00:32 +0000 (09:00 +0000)
commitc44be86afb9b9811e59ebdd0fc5819e029b66207
tree9469b5ecf036ab0de3ed248241179044f2338641tree | snapshot
parent650e3b3c9ff0b9cafb76a0edf8139a53446937bacommit | diff
Partial bug fix: every inner type is now added to the selection roots.
However, the inner types are not closed terms! They live in the context of
their terms. Right now there is a bug in locating subterms of a proof.
Thus I do not even try to fix inner types selection properly.
helm/matita/matitaMathView.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.