matita.cs.unibo.it Git - helm.git/commit

]> matita.cs.unibo.it Git - helm.git/commit

author	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Mon, 25 Sep 2006 16:52:53 +0000 (16:52 +0000)
committer	Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
	Mon, 25 Sep 2006 16:52:53 +0000 (16:52 +0000)
commit	070e79b6e7ec986dd5fcdee24857956f6a4a9221
tree	284f93651e0b586515ee9953b1ef37719efef0f6	tree \| snapshot
parent	d723cac1efffbc8ef3ffcbaa96a2c390e2b8780e	commit \| diff

injection_tac and discriminate_tac now replaced by destruct_tac that
performs either injection or discrimination. In Coq destruct is called
"analyze equality".

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom

components/grafite/grafiteAst.ml		diff \| blob \| history
components/grafite/grafiteAstPp.ml		diff \| blob \| history
components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
components/grafite_parser/grafiteDisambiguate.ml		diff \| blob \| history
components/grafite_parser/grafiteParser.ml		diff \| blob \| history
matita/help/C/sec_tactics.xml		diff \| blob \| history
matita/help/C/tactic_quickref.xml		diff \| blob \| history
matita/matita.lang		diff \| blob \| history
matita/tests/dependent_injection.ma	[new file with mode: 0644]	blob
matita/tests/discriminate.ma		diff \| blob \| history
matita/tests/injection.ma		diff \| blob \| history