]> matita.cs.unibo.it Git - helm.git/commit
Disambiguation errors in phase 3 that are not present in phase 4 are filtered
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Dec 2006 11:39:07 +0000 (11:39 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 8 Dec 2006 11:39:07 +0000 (11:39 +0000)
commitce00fb7749b1bf3bc2e68e578bf945fdcd302926
tree41fca94ca1644e2c166c8089c64a4fcbe5bd1246
parent2caabc2c2021d86911f8df8ee92d230c5e4e0389
Disambiguation errors in phase 3 that are not present in phase 4 are filtered
out. Explanation: if they are only in phase 3, it means that in phase 4 they
are not significative. Thus we conclude that phase 3 is not significative.
There is a drawback: equality over errors is not very well defined because
of Metas in error messages. Thus it could be the case that we remove the error
in phase 3 when the same error is still there in phase 4.
helm/software/matita/matitaGui.ml