]> matita.cs.unibo.it Git - helm.git/commit
added include' to include everything but preferences (aka aliases)
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 13 Apr 2006 14:24:03 +0000 (14:24 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 13 Apr 2006 14:24:03 +0000 (14:24 +0000)
commitb95be966e385957a25f26a41f45e0116955264ae
tree9ad0599f220a209a14ddc3bba6b0e2635b582b52
parent780561e45e8de50dd0063a0e369458ba67479872
added include' to include everything but preferences (aka aliases)
helm/software/components/grafite_parser/dependenciesParser.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/lexicon/lexiconAst.ml
helm/software/components/lexicon/lexiconAstPp.ml
helm/software/components/lexicon/lexiconEngine.ml