]> matita.cs.unibo.it Git - helm.git/commit
1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Jul 2005 15:41:15 +0000 (15:41 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 28 Jul 2005 15:41:15 +0000 (15:41 +0000)
commit6531c263da005e25ea2f58f9ee960acba7857ff6
treedd2ac1ccd6c60f0bdbb43bc12e1cda31e4e136da
parentd73bd6d966d4aeb509a3cf776708d55560464ec2
1. ProofEngineHelpers.locate_in_term, ProofEngineHelpers.locate_in_conjecture
   generalized to return the list of matched terms
2. unfold generalized to unfold several occurrences at once
helm/matita/matitaEngine.ml
helm/matita/matitaMathView.ml
helm/matita/tests/unfold.ma
helm/ocaml/tactics/proofEngineHelpers.ml
helm/ocaml/tactics/proofEngineHelpers.mli
helm/ocaml/tactics/proofEngineReduction.ml
helm/ocaml/tactics/reductionTactics.ml
helm/ocaml/tactics/reductionTactics.mli
helm/ocaml/tactics/tactics.mli