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