]> matita.cs.unibo.it Git - helm.git/commit
injection_tac and discriminate_tac now replaced by destruct_tac
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Sep 2006 16:54:35 +0000 (16:54 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Sep 2006 16:54:35 +0000 (16:54 +0000)
commit2686842a2780bffbe6b317e0fd3fdfa0a4370a48
tree9929e691d647f3ae1572d542177b6f886e31b09f
parent070e79b6e7ec986dd5fcdee24857956f6a4a9221
injection_tac and discriminate_tac now replaced by destruct_tac
components/tactics/discriminationTactics.ml
components/tactics/discriminationTactics.mli
components/tactics/tactics.ml
components/tactics/tactics.mli