]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9a9c5b8) | patch
Bug fixed: pretty-printing of aliases when the OK button is pressed in the
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 Dec 2008 12:36:44 +0000 (12:36 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 4 Dec 2008 12:36:44 +0000 (12:36 +0000)
commit9ead65f0b6b17fc8f01ffcb977c3c252594724a9
treee7c342b421e5b4fc4a9e63abf9d667fa5e1e4d31tree | snapshot
parent9a9c5b863f68367119450ae7b806d454ba1265e3commit | diff
Bug fixed: pretty-printing of aliases when the OK button is pressed in the
ambiguous error window.
helm/software/components/lexicon/disambiguatePp.ml diff | blob | history
helm/software/components/lexicon/disambiguatePp.mli diff | blob | history
helm/software/matita/matitaGui.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.