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

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

author	Enrico Tassi <enrico.tassi@inria.fr>
	Mon, 10 Jul 2006 17:07:24 +0000 (17:07 +0000)
committer	Enrico Tassi <enrico.tassi@inria.fr>
	Mon, 10 Jul 2006 17:07:24 +0000 (17:07 +0000)
commit	27ce29cfef1e71c00ee19d2c00c9f425f9efb031
tree	6360b62bbd1e95dfb8cb0cb3f38c862df4fdb4d9	tree \| snapshot
parent	20739bf5dca88698f081f1253355f109a6955077	commit \| diff

improved coercions support:
- multiple coercions from the same carrier are allowed
- coercions are hidden from the proof too
- a new function to print proof in text mode added

19 files changed:

components/acic_content/acic2content.ml		diff \| blob \| history
components/acic_content/acic2content.mli		diff \| blob \| history
components/acic_content/termAcicContent.ml		diff \| blob \| history
components/acic_content/termAcicContent.mli		diff \| blob \| history
components/cic_unification/cicRefine.ml		diff \| blob \| history
components/content_pres/.depend		diff \| blob \| history
components/content_pres/Makefile		diff \| blob \| history
components/content_pres/boxPp.ml		diff \| blob \| history
components/content_pres/boxPp.mli		diff \| blob \| history
components/content_pres/cicNotationLexer.ml		diff \| blob \| history
components/content_pres/objPp.ml	[new file with mode: 0644]	blob
components/content_pres/objPp.mli	[new file with mode: 0644]	blob
components/grafite_engine/grafiteEngine.ml		diff \| blob \| history
components/library/cicCoercion.ml		diff \| blob \| history
components/library/coercDb.ml		diff \| blob \| history
components/library/coercDb.mli		diff \| blob \| history
components/library/coercGraph.ml		diff \| blob \| history
components/library/coercGraph.mli		diff \| blob \| history
components/library/librarySync.ml		diff \| blob \| history

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

RSS Atom