]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 001b43b) | patch
1. More debugging code
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Jan 2007 19:00:34 +0000 (19:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 2 Jan 2007 19:00:34 +0000 (19:00 +0000)
commit4480f2625fce077f7389dde595920d25748820eb
tree4c6bf4ffbdb0179a69423971fd1bbd6ce6fe2d63tree | snapshot
parent001b43beae9e912a921da426d23c1e437328bb9ecommit | diff
1. More debugging code
2. "Bug" "fixed": when the pullback of two coercions is computed, only the
   join is returned, but not the two coercions that complete the pullback.
   Thus we need to recompute them and it may happen that we find more than one
   parallel coercions. This "fix" just randomly picks the first one (instead
   of raising an assert false). All this stuff must be handled in a better way.
components/cic_unification/cicUnification.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.