]> matita.cs.unibo.it Git - helm.git/commit
A few other tactics made available to matita.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Jun 2005 16:57:10 +0000 (16:57 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 27 Jun 2005 16:57:10 +0000 (16:57 +0000)
commitdf0606d3bcbc41272fcde2d013bbe0b1aadf98af
tree084ebe236196842e43baab6e7d6144c0b0df8c72
parentded3a0b12793fc8e463a4a3be9f62f54f734897e
A few other tactics made available to matita.
A few tactics (change, fold, replace) generalized to patterns.
The argument of clear and clearbody is now an identifier.

WARNING: the implementation of change, fold and replace has been commented
out to generalize them to patterns. To be committed soon.
20 files changed:
helm/ocaml/cic_disambiguation/cicTextualParser2.ml
helm/ocaml/cic_transformations/tacticAst.ml
helm/ocaml/cic_transformations/tacticAst2Box.ml
helm/ocaml/cic_transformations/tacticAstPp.ml
helm/ocaml/tactics/eliminationTactics.ml
helm/ocaml/tactics/equalityTactics.ml
helm/ocaml/tactics/equalityTactics.mli
helm/ocaml/tactics/fourierR.ml
helm/ocaml/tactics/primitiveTactics.mli
helm/ocaml/tactics/proofEngineStructuralRules.ml
helm/ocaml/tactics/proofEngineStructuralRules.mli
helm/ocaml/tactics/reductionTactics.ml
helm/ocaml/tactics/reductionTactics.mli
helm/ocaml/tactics/ring.ml
helm/ocaml/tactics/tacticals.ml
helm/ocaml/tactics/tacticals.mli
helm/ocaml/tactics/tactics.ml
helm/ocaml/tactics/tactics.mli
helm/ocaml/tactics/variousTactics.ml
helm/ocaml/tactics/variousTactics.mli