]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a8c5f68) | 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)
commit0ffad67d97b1495a4444e2cf2dbd82f882ed15e9
treedf52f9e707d5af0aeb42c7c6604a60040b75406etree | snapshot
parenta8c5f68fcefade4fa759c588a3cfb67277f66530commit | 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).
components/cic_unification/cicRefine.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.