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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Fri, 26 Sep 2008 16:38:29 +0000 (16:38 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Fri, 26 Sep 2008 16:38:29 +0000 (16:38 +0000)
commit	01001c883a8151edba81cd03a6f254d24a81c867
tree	239b40eee5a214474af6af3b60143f3325166b48	tree \| snapshot
parent	ea3b15fdedb39c72ae1b39f210917c6f38fc062d	commit \| diff

more push/pop to avoid confusion with imperative data structures employed by
notation. the patch is not well tested, but already improves the situation
make the library compile again. I commit it so that on monday we will have
again the livecd and the .dsb package that are required by the sysadmins to
install matita on the cs cluster

12 files changed:

helm/software/components/content_pres/cicNotationLexer.ml		diff \| blob \| history
helm/software/components/content_pres/cicNotationLexer.mli		diff \| blob \| history
helm/software/components/content_pres/cicNotationParser.ml		diff \| blob \| history
helm/software/components/content_pres/cicNotationParser.mli		diff \| blob \| history
helm/software/components/content_pres/test_lexer.ml		diff \| blob \| history
helm/software/components/grafite_parser/dependenciesParser.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.mli		diff \| blob \| history
helm/software/components/grafite_parser/print_grammar.ml		diff \| blob \| history
helm/software/components/lexicon/cicNotation.ml		diff \| blob \| history
helm/software/matita/matitaScript.ml		diff \| blob \| history
helm/software/matita/matitacLib.ml		diff \| blob \| history

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

RSS Atom