]> matita.cs.unibo.it Git - helm.git/commit
All the tactics have been ported to use the objects in LibraryObjects.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Jul 2005 12:30:36 +0000 (12:30 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Jul 2005 12:30:36 +0000 (12:30 +0000)
commitb8ac0d11d5cd4083838a3848fce68683a518b54a
treefcac7a0e4ba76c3ef257996313184e1166d5967e
parentce1f4abf56632f8fef8368073d3f6728cf2655c1
All the tactics have been ported to use the objects in LibraryObjects.
helm/ocaml/cic/libraryObjects.ml
helm/ocaml/cic/libraryObjects.mli
helm/ocaml/cic/matitaLibraryObjects.ml
helm/ocaml/cic/matitaLibraryObjects.mli
helm/ocaml/tactics/discriminationTactics.ml
helm/ocaml/tactics/negationTactics.ml