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