matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Enrico Tassi <enrico.tassi@inria.fr>
	Thu, 4 Dec 2008 13:06:29 +0000 (13:06 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Thu, 4 Dec 2008 13:06:29 +0000 (13:06 +0000)
commit	c04f852241510515f06e3bec8eb79acac6e4952e
tree	bba896b7601201e3d1be8ab332deb9fd19a304b3	tree \| snapshot
parent	9ead65f0b6b17fc8f01ffcb977c3c252594724a9	commit \| diff

housekeeping:
- unused functions removed from Enviconment
- unused file disambiguatePp removed
- disambiguation callbacks pushed down to Disambiguate
from MultiPassDisambiguator

13 files changed:

helm/software/components/disambiguation/disambiguate.ml		diff \| blob \| history
helm/software/components/disambiguation/disambiguate.mli		diff \| blob \| history
helm/software/components/disambiguation/disambiguateTypes.ml		diff \| blob \| history
helm/software/components/disambiguation/disambiguateTypes.mli		diff \| blob \| history
helm/software/components/disambiguation/multiPassDisambiguator.ml		diff \| blob \| history
helm/software/components/disambiguation/multiPassDisambiguator.mli		diff \| blob \| history
helm/software/components/lexicon/.depend		diff \| blob \| history
helm/software/components/lexicon/.depend.opt		diff \| blob \| history
helm/software/components/lexicon/Makefile		diff \| blob \| history
helm/software/components/lexicon/disambiguatePp.ml	[deleted file]	blob \| history
helm/software/components/lexicon/disambiguatePp.mli	[deleted file]	blob \| history
helm/software/matita/matitaGui.ml		diff \| blob \| history
helm/software/matita/matitaScript.ml		diff \| blob \| history

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom