]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 057a399) | patch
- disambiguation code moved from matitaEngine to grafiteDisambiguate
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 4 Nov 2010 23:10:56 +0000 (23:10 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 4 Nov 2010 23:10:56 +0000 (23:10 +0000)
commitdc04177512e6db696f669aa561b86701c4ad2511
tree074cb9fd48f8fce9c6c69644394d4e02c3d7b97ftree | snapshot
parent057a399c7f497cde3a09cd46505a441d2d6bacc7commit | diff
- disambiguation code moved from matitaEngine to grafiteDisambiguate
- grafiteDisambiguate.db is now opaque
matita/components/grafite_engine/grafiteEngine.ml diff | blob | history
matita/components/lexicon/grafiteDisambiguate.ml diff | blob | history
matita/components/lexicon/grafiteDisambiguate.mli diff | blob | history
matita/matita/matitaEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.