]> matita.cs.unibo.it Git - helm.git/commit
Bugged code patched, but not in the optimal way.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Dec 2006 18:50:09 +0000 (18:50 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Dec 2006 18:50:09 +0000 (18:50 +0000)
commit7bf7eb896d5d450655d99dd78bd2a3a66b17ea1a
treebdc959887ac5cdde0cb4a006f9b5d79ddc3a22c4
parent5aa1f1918c39c0d4130574927fa0f870e613cdea
Bugged code patched, but not in the optimal way.
The problem is that in two different interpretations a symbol id can be
interpreted as dsc in different locations. Using the previous code it
happened that every interpretation was pruned out since a symbol id occurred
twice (in different locations) in an/every interpretation. Now the couples
(loc,id) are considered for disambiguating between the two interpretations.
However, this way we hide information to the user (what other occurrences of
the same symbol are given the same interpretation).
matita/matitaGui.ml