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

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

Declarative tactics for rewriting steps, elimination of the existential
quantifier and elimination of conjunciton implemented.

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

helm/software/components/grafite/grafiteAst.ml		diff \| blob \| history
helm/software/components/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/software/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteDisambiguate.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/tactics/declarative.ml		diff \| blob \| history
helm/software/components/tactics/declarative.mli		diff \| blob \| history
helm/software/matita/matita.lang		diff \| blob \| history
helm/software/matita/tests/decl.ma		diff \| blob \| history