]> matita.cs.unibo.it Git - helm.git/commit
improved coercions support:
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 10 Jul 2006 17:07:24 +0000 (17:07 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 10 Jul 2006 17:07:24 +0000 (17:07 +0000)
commitbdf989481462c1185c9cbbfdd4b31d13aa4352b3
tree8d3ae4fcfe27beee717179f097e0e44510eaabb3
parent494d586c56cf3ecfcd2b495c5bb10d8b26260340
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:
helm/software/components/acic_content/acic2content.ml
helm/software/components/acic_content/acic2content.mli
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/acic_content/termAcicContent.mli
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/content_pres/.depend
helm/software/components/content_pres/Makefile
helm/software/components/content_pres/boxPp.ml
helm/software/components/content_pres/boxPp.mli
helm/software/components/content_pres/cicNotationLexer.ml
helm/software/components/content_pres/objPp.ml [new file with mode: 0644]
helm/software/components/content_pres/objPp.mli [new file with mode: 0644]
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/library/cicCoercion.ml
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/coercGraph.ml
helm/software/components/library/coercGraph.mli
helm/software/components/library/librarySync.ml