]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: df1201e) | patch
Stricter type: the type now shows that disambiguation only alter the lexicon.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Jun 2009 09:17:53 +0000 (09:17 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 18 Jun 2009 09:17:53 +0000 (09:17 +0000)
commit7477c3dbbc2fafe248d48302be0d6ba4cb38d062
tree2ad3344519c1a00e7617745214fda96eb9ce786etree | snapshot
parentdf1201e37d6f2631dc31ffc87b979a6c81180a3acommit | diff
Stricter type: the type now shows that disambiguation only alter the lexicon.
In this way we are forced to manually set the content of the object in place of
setting the whole object, that leads to information loss since in the meanwhile
new commands may have altered the rest of the state.
helm/software/components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/software/components/grafite_parser/grafiteDisambiguate.mli diff | blob | history
helm/software/matita/matitaEngine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.