]> 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)
commit4f2e7eacea9e8b3089a575d7bf529fd5e70e8453
tree1fa3850849f8d77af968cd43a07507af26369924
parent9c67eded501cab6f8284d9afb3a3fcbeb8f8ec8b
COERCIONS: tentative addition of an equivalence relation over coercion source
carriers (convertibility) for the moment used only in the FunClass case.
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/cic_unification/coercGraph.ml
helm/software/components/cic_unification/coercGraph.mli
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/tactics/closeCoercionGraph.ml