]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 12ebc94) | patch
Disambiguation error compaction is now performed in the same way by matita and
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 26 Nov 2007 11:54:52 +0000 (11:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 26 Nov 2007 11:54:52 +0000 (11:54 +0000)
commit1df136280cced19d29b62451c8c03948070259d8
treeaf2904c5c4e588ab4b0b8b88c7b002d57ca8523ctree | snapshot
parent12ebc9483bec78f948de80e7e230c98488890f4dcommit | diff
Disambiguation error compaction is now performed in the same way by matita and
matitac. The difference is that matitac shows every error in every pass,
marking spurious errors as spurious.
helm/software/matita/matitaExcPp.ml diff | blob | history
helm/software/matita/matitaExcPp.mli diff | blob | history
helm/software/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.