]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 213cac2) | patch
GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 28 Oct 2006 17:12:31 +0000 (17:12 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 28 Oct 2006 17:12:31 +0000 (17:12 +0000)
commiteb41d84ee7ee6a53e35dd08e7fbf5d51f3972c4c
tree66324cf31a71955dec70a5317e23437a16338631tree | snapshot
parent213cac2ec31720d1988c990a4c4ef04d47bb2ff9commit | diff
GRAVE BUG IN COERCIONS FIXED: the insertion of a coercion used to introduce
applications of applications (that are forbidden and not handled properly).
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.