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

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

author	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 6 Nov 2007 19:30:16 +0000 (19:30 +0000)
committer	Ferruccio Guidi <ferruccio.guidi@unibo.it>
	Tue, 6 Nov 2007 19:30:16 +0000 (19:30 +0000)
commit	ef870606391fff198f215127eb022eb3e41ab1d4
tree	76b594fa9d5648b87d1810ff939897d1e6dbeec7	tree \| snapshot
parent	040b70279b9bf0f576f00a9b1ad28df3c8bf6024	commit \| diff

new implementation of the destruct tactic,
which includes the old subst tactic (now removed)

24 files changed:

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
components/tactics/.depend		diff \| blob \| history
components/tactics/.depend.opt		diff \| blob \| history
components/tactics/Makefile		diff \| blob \| history
components/tactics/destructTactic.ml	[new file with mode: 0644]	blob
components/tactics/destructTactic.mli	[new file with mode: 0644]	blob
components/tactics/discriminationTactics.ml	[deleted file]	blob \| history
components/tactics/discriminationTactics.mli	[deleted file]	blob \| history
components/tactics/substTactic.ml	[deleted file]	blob \| history
components/tactics/substTactic.mli	[deleted file]	blob \| history
components/tactics/tactics.ml		diff \| blob \| history
components/tactics/tactics.mli		diff \| blob \| history
matita/library/Fsub/defn.ma		diff \| blob \| history
matita/library/Fsub/part1a.ma		diff \| blob \| history
matita/library/Fsub/part1a_inversion.ma		diff \| blob \| history
matita/library/Fsub/util.ma		diff \| blob \| history
matita/library/Z/z.ma		diff \| blob \| history
matita/library/decidable_kit/fgraph.ma		diff \| blob \| history
matita/library/decidable_kit/list_aux.ma		diff \| blob \| history
matita/tests/destruct.ma		diff \| blob \| history

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