]> 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)
commit7e1af5926cf614736c0575a4a3ae2c3cc3b26924
treefaf1512d6030ed206a7e96bc4a67addbd6dd71c9
parentccd1ec9a248921b2c81817b1a7f6f0a2f27d5c32
injection_tac and discriminate_tac now replaced by destruct_tac
helm/software/components/tactics/discriminationTactics.ml
helm/software/components/tactics/discriminationTactics.mli
helm/software/components/tactics/tactics.ml
helm/software/components/tactics/tactics.mli