]> 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)
commit918b39ec5f3477499230c7370d4798f20a65cd8d
tree5b0f27c18d582843806622c2e50dec6fdd7a1f46
parent971a1e0f0c80f1165ff2c5ba956702f41819cac4
added include' to include everything but preferences (aka aliases)
components/grafite_parser/dependenciesParser.ml
components/grafite_parser/grafiteParser.ml
components/lexicon/lexiconAst.ml
components/lexicon/lexiconAstPp.ml
components/lexicon/lexiconEngine.ml