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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Sun, 6 Jan 2008 15:48:38 +0000 (15:48 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Sun, 6 Jan 2008 15:48:38 +0000 (15:48 +0000)
commit	4a62bde42e3655a7829b9281d9b9057dc32c0471
tree	36354c80b650666145075edf92c7b3880258d93b	tree \| snapshot
parent	c780c9756b67d116b1d5b5149ae758fa613c5fe6	commit \| diff

irediced usage of matita.includes, that is now set by
matitaInit and should be read once at the beginning of every
main, removed rottener

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

components/grafite_parser/grafiteParser.ml		diff \| blob \| history
components/grafite_parser/grafiteWalker.ml		diff \| blob \| history
components/grafite_parser/grafiteWalker.mli		diff \| blob \| history
components/library/librarian.ml		diff \| blob \| history
components/library/librarian.mli		diff \| blob \| history
matita/matitaScript.ml		diff \| blob \| history
matita/matitac.ml		diff \| blob \| history
matita/matitacLib.ml		diff \| blob \| history
matita/matitaclean.ml		diff \| blob \| history
matita/matitadep.ml		diff \| blob \| history
matita/rottener.ml	[deleted file]	blob \| history