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