]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c5f2c1c) | patch
Serious bug fixed: the types of a real mutual fix definition were not lifted
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 2 Feb 2007 18:15:59 +0000 (18:15 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 2 Feb 2007 18:15:59 +0000 (18:15 +0000)
commita95bb53a77f84592a64131eadf7d4501c49667ce
treedf2945d7e6a39558cef42a0e8010b2d1192b7d55tree | snapshot
parentc5f2c1c89032b6b65499de04af9f2b7428059c67commit | diff
Serious bug fixed: the types of a real mutual fix definition were not lifted
as required. Moreover, an unification exception used to escape the refiner.
Now it does no more, but the error is not localized (being about the branch
of a MutCase that has no precise localization).
helm/software/components/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.