]> matita.cs.unibo.it Git - helm.git/commit
tentative parser patch with symbolic tactics names
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 22 Oct 2010 15:59:56 +0000 (15:59 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 22 Oct 2010 15:59:56 +0000 (15:59 +0000)
commitcb11de1c61f0b61935b1c6c1832deacb49f7b5bd
tree41926ec0fabbdf79dc1ffdcdad18c61cdb59e29a
parent4f644cf056ebf420cc298dbdabd5a907da9fd5d3
tentative parser patch with symbolic tactics names
matita/components/grafite_parser/grafiteParser.ml
matita/matita/matita.lang