]> matita.cs.unibo.it Git - helm.git/commit
the decompose tactic is now working
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 19 Jul 2005 10:26:24 +0000 (10:26 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 19 Jul 2005 10:26:24 +0000 (10:26 +0000)
commitcb473667ca89549ed0ca6dd2bfb03a5fe9eeaa82
tree56535800ab5d15399c1e981f4c72ce1deac6d6b7
parent0d498c2c58dec9a024a489c902e463b1cac4a1b0
the decompose tactic is now working
16 files changed:
helm/matita/matita.ma.templ
helm/matita/matitaEngine.ml
helm/matita/tests/fguidi.ma
helm/ocaml/cic_notation/grafiteAst.ml
helm/ocaml/cic_notation/grafiteAstPp.ml
helm/ocaml/cic_notation/grafiteParser.ml
helm/ocaml/cic_transformations/tacticAst.ml
helm/ocaml/cic_transformations/tacticAstPp.ml
helm/ocaml/tactics/eliminationTactics.ml
helm/ocaml/tactics/eliminationTactics.mli
helm/ocaml/tactics/fwdSimplTactic.ml
helm/ocaml/tactics/metadataQuery.ml
helm/ocaml/tactics/metadataQuery.mli
helm/ocaml/tactics/proofEngineHelpers.ml
helm/ocaml/tactics/proofEngineHelpers.mli
helm/ocaml/tactics/tactics.mli