The Coq mailing list

[Cyril Cohen <cohen AT crans.org>]

Hi,

Le 14/12/2010 16:29, Carsten Varming a écrit :
> This is exactly the same problem as above. Adding this does the trick:
> [...]

Thanks, I did not think of adding several morphism declaration for the
same operator. I guess this could solve my entire problem now.
However, I would have to declare hundreds of morphisms: I have at least
5 canonical structures to take into account, for more than 10 operators,
most of which are binary !

>> Since (sort' (str_str' T)) and sort T are convertible, why does the
>> resolution fail ?
> 
> I don't know. You would think that evaluating types to a normal form
> would be the right thing to do, but that not the way it is currently done.

Or by unification modulo conversion between the given type and the
expected one. That's what I thought was done, but I don't understand
fully the problem.

Cheers,
-- 
Cyril Cohen
sorry for the double mailing ...