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: 798e85c) | 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	3990759a81db3ce45bf4ec56e1985e532151f6e0
tree	76c04b4099b7ed2436c6e8c04dbac04a19bcd651	tree \| snapshot
parent	798e85cb6d55d80d988f91e6289e4041e95ad2e4	commit \| diff

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

17 files changed:

helm/software/components/grafite/grafiteAst.ml		diff \| blob \| history
helm/software/components/grafite/grafiteAstPp.ml		diff \| blob \| history
helm/software/components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteDisambiguate.ml		diff \| blob \| history
helm/software/components/grafite_parser/grafiteParser.ml		diff \| blob \| history
helm/software/components/library/cicCoercion.ml		diff \| blob \| history
helm/software/components/library/cicCoercion.mli		diff \| blob \| history
helm/software/components/tactics/.depend		diff \| blob \| history
helm/software/components/tactics/.depend.opt		diff \| blob \| history
helm/software/components/tactics/Makefile		diff \| blob \| history
helm/software/components/tactics/closeCoercionGraph.ml	[new file with mode: 0644]	blob
helm/software/components/tactics/closeCoercionGraph.mli	[new file with mode: 0644]	blob
helm/software/components/tactics/compose.ml	[new file with mode: 0644]	blob
helm/software/components/tactics/compose.mli	[new file with mode: 0644]	blob
helm/software/components/tactics/tactics.ml		diff \| blob \| history
helm/software/components/tactics/tactics.mli		diff \| blob \| history
helm/software/matita/matita.lang		diff \| blob \| history

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