]> matita.cs.unibo.it Git - helm.git/commitdiff
projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (from: c837217)
Coercion hiding implemented. Notes:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 13 Jul 2009 03:27:46 +0000 (03:27 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 13 Jul 2009 03:27:46 +0000 (03:27 +0000)
1) hiding of coercions whose return type is a product is not done correctly,
   since the "sats" information seem to have changed semantics. Enrico, is it
   a bug or just a new semantics?
2) coercion matching has been implemented trivially (O(n)) in NCicCoercion.
   Here I need a special version of a discrimination tree. Enrico, do we have
   one already or is there a way to simulate it?


No differences found
Unnamed repository; edit this file 'description' to name the repository.