]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d7227b9) | patch
experimental classification of disambiguation error, so that supposedly non significa...
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 5 Dec 2006 17:11:23 +0000 (17:11 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 5 Dec 2006 17:11:23 +0000 (17:11 +0000)
commit45ac0bf0fb6c58e03646588d4f81cf5125058e67
tree2546c85e2aa9f70589d9ee4bd8b6c7038aa612c4tree | snapshot
parentd7227b93729c13636d297b959b7d8c178dfe3aafcommit | diff
experimental classification of disambiguation error, so that supposedly non significant errors can be hidden to the user
ATM an error is non significant if obtained interpretating a symbol that can be interpreted in an error-free way
components/cic_disambiguation/disambiguate.ml diff | blob | history
components/cic_disambiguation/disambiguate.mli diff | blob | history
components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
components/grafite_parser/grafiteDisambiguator.ml diff | blob | history
components/grafite_parser/grafiteDisambiguator.mli diff | blob | history
matita/matitaExcPp.ml diff | blob | history
matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.