]> matita.cs.unibo.it Git - helm.git/commit
COERCIONS: tentative addition of an equivalence relation over coercion source
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 19 Jul 2007 10:03:42 +0000 (10:03 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 19 Jul 2007 10:03:42 +0000 (10:03 +0000)
commit975ad45cc779a6bee3d450a006347cc23ca3977e
tree452b5b5d3ca4afa43c21c27abc5b6a421b25d6c0
parent51e73d704c8397356644af767ae936e4b3a82dbe
COERCIONS: tentative addition of an equivalence relation over coercion source
carriers (convertibility) for the moment used only in the FunClass case.
components/cic_unification/cicRefine.ml
components/cic_unification/coercGraph.ml
components/cic_unification/coercGraph.mli
components/library/coercDb.ml
components/library/coercDb.mli
components/tactics/closeCoercionGraph.ml