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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Wed, 26 Nov 2008 16:11:47 +0000 (16:11 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Wed, 26 Nov 2008 16:11:47 +0000 (16:11 +0000)
commit	1d212933a86f2820a151555516f7a53ab1c9f8e7
tree	2b72ca3b8393784665e772f488a7cf660299bef6	tree \| snapshot
parent	92c4af96b3c1e4918bdc10b7cbdb3a37038de074	commit \| diff

disambiguation even more abstracted

23 files changed:

helm/software/components/cic_disambiguation/disambiguate.ml		diff \| blob \| history
helm/software/components/cic_disambiguation/disambiguate.mli		diff \| blob \| history
helm/software/components/cic_disambiguation/disambiguateChoices.mli		diff \| blob \| history
helm/software/components/cic_disambiguation/disambiguateTypes.ml		diff \| blob \| history
helm/software/components/cic_disambiguation/disambiguateTypes.mli		diff \| blob \| history
helm/software/components/grafite_parser/cicNotation2.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/components/lexicon/disambiguatePp.mli		diff \| blob \| history
helm/software/components/lexicon/lexiconEngine.ml		diff \| blob \| history
helm/software/components/lexicon/lexiconEngine.mli		diff \| blob \| history
helm/software/components/lexicon/lexiconSync.mli		diff \| blob \| history
helm/software/components/ng_disambiguation/.depend		diff \| blob \| history
helm/software/components/ng_disambiguation/.depend.opt	[new file with mode: 0644]	blob
helm/software/components/ng_disambiguation/Makefile		diff \| blob \| history
helm/software/components/ng_disambiguation/nDisambiguate.ml		diff \| blob \| history
helm/software/components/ng_disambiguation/nDisambiguate.mli		diff \| blob \| history
helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml	[new file with mode: 0644]	blob
helm/software/components/ng_disambiguation/nGrafiteDisambiguator.mli	[new file with mode: 0644]	blob
helm/software/matita/matitaEngine.mli		diff \| blob \| history
helm/software/matita/matitaExcPp.mli		diff \| blob \| history
helm/software/matita/matitaGui.ml		diff \| blob \| history

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

RSS Atom