]> matita.cs.unibo.it Git - helm.git/commit
All the reduction tactics have been modified to reduce several (sub)terms
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jan 2003 13:20:00 +0000 (13:20 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 29 Jan 2003 13:20:00 +0000 (13:20 +0000)
commit146f8a58cd8c9aebe3d49df7f09e921f43c0c0e8
tree095442765e995e3368c0d6effde2392111cef89c
parenta13f87720761d95ab36b49284e7530bbd7e694ff
All the reduction tactics have been modified to reduce several (sub)terms
at once.
helm/ocaml/tactics/equalityTactics.ml
helm/ocaml/tactics/primitiveTactics.ml
helm/ocaml/tactics/proofEngineReduction.ml
helm/ocaml/tactics/proofEngineReduction.mli
helm/ocaml/tactics/reductionTactics.ml
helm/ocaml/tactics/reductionTactics.mli