]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 494d586) | patch
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
tree8d3ae4fcfe27beee717179f097e0e44510eaabb3tree | snapshot
parent494d586c56cf3ecfcd2b495c5bb10d8b26260340commit | 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:
helm/software/components/acic_content/acic2content.ml diff | blob | history
helm/software/components/acic_content/acic2content.mli diff | blob | history
helm/software/components/acic_content/termAcicContent.ml diff | blob | history
helm/software/components/acic_content/termAcicContent.mli diff | blob | history
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
helm/software/components/content_pres/.depend diff | blob | history
helm/software/components/content_pres/Makefile diff | blob | history
helm/software/components/content_pres/boxPp.ml diff | blob | history
helm/software/components/content_pres/boxPp.mli diff | blob | history
helm/software/components/content_pres/cicNotationLexer.ml diff | blob | history
helm/software/components/content_pres/objPp.ml [new file with mode: 0644] blob
helm/software/components/content_pres/objPp.mli [new file with mode: 0644] blob
helm/software/components/grafite_engine/grafiteEngine.ml diff | blob | history
helm/software/components/library/cicCoercion.ml diff | blob | history
helm/software/components/library/coercDb.ml diff | blob | history
helm/software/components/library/coercDb.mli diff | blob | history
helm/software/components/library/coercGraph.ml diff | blob | history
helm/software/components/library/coercGraph.mli diff | blob | history
helm/software/components/library/librarySync.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.