]> matita.cs.unibo.it Git - helm.git/commit
support -axiom to avoind indexing an axiom (since there is no qed)
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 12 Dec 2011 20:14:53 +0000 (20:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 12 Dec 2011 20:14:53 +0000 (20:14 +0000)
commitf5b9e1d5511a13ca5bb424c149781087aa0c8e31
treed02e022dc6bd14a896447fb33800ac22f180ba45
parent8344b3062fc040a7565e43b646d12197d1d51ee3
support -axiom to avoind indexing an axiom (since there is no qed)
matita/components/grafite/grafiteAst.ml
matita/components/grafite/grafiteAstPp.ml
matita/components/grafite_engine/grafiteEngine.ml
matita/components/grafite_parser/grafiteParser.ml