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

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

projects / helm.git / commit

summary | shortlog | log | commit | commitdiff | tree
(parent: ce5018f) | patch

author	Enrico Tassi <enrico.tassi@inria.fr>
	Fri, 1 Jun 2007 14:58:50 +0000 (14:58 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Fri, 1 Jun 2007 14:58:50 +0000 (14:58 +0000)
commit	936f80cf031a7b034dd70fef49abb90e69f2e680
tree	92b70993cf6e77ab3eed64297e322a25587d704a	tree \| snapshot
parent	ce5018fb3004d79fd16301dfc0fd9370d59ba4fc	commit \| diff

new compose tactic, still undocumented.
moved from library to tactics the code for composing coercions.

17 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/library/cicCoercion.ml		diff \| blob \| history
components/library/cicCoercion.mli		diff \| blob \| history
components/tactics/.depend		diff \| blob \| history
components/tactics/.depend.opt		diff \| blob \| history
components/tactics/Makefile		diff \| blob \| history
components/tactics/closeCoercionGraph.ml	[new file with mode: 0644]	blob
components/tactics/closeCoercionGraph.mli	[new file with mode: 0644]	blob
components/tactics/compose.ml	[new file with mode: 0644]	blob
components/tactics/compose.mli	[new file with mode: 0644]	blob
components/tactics/tactics.ml		diff \| blob \| history
components/tactics/tactics.mli		diff \| blob \| history
matita/matita.lang		diff \| blob \| history

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