]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b467000) | 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)
commit8b20a402003f57320cb9f0cc2eedebbceb16d3fc
treeefc7c2770fb270ef448905a58c004ed816ee89b6tree | snapshot
parentb4670008138505f7462252c29eb755ab127862bacommit | 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
helm/software/components/cic_disambiguation/disambiguate.ml diff | blob | history
helm/software/components/cic_disambiguation/disambiguate.mli diff | blob | history
helm/software/components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/software/components/grafite_parser/grafiteDisambiguator.ml diff | blob | history
helm/software/components/grafite_parser/grafiteDisambiguator.mli diff | blob | history
helm/software/matita/matitaExcPp.ml diff | blob | history
helm/software/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.