The Coq mailing list

[David Pereira <dpereira AT liacc.up.pt>]

Hi again,
>> Hope it helps,
> 
> It does. Thanks!

You are welcome :)
> 
> 
>> Did you tried [Check @map]. I have not tried exhaustively with containers 
>> in
>> 8.4, but I suspect the problem may be with Coq trying to find an instance
>> to the definition of [map].
> 
> I may have been a bit rash to consult coq-club: dict is the analogue of 
> set; 
> map is of course just the "mapping" function so it needs an FMap instance 
> in 
> context.

Just an opinion: two of my developments make intensive use of finite sets, 
not so much of maps. But one this I have noticed when porting such 
developments to Coq 8.4 was that the compilation process become much slower, 
when compared to Coq 8.3. I think that this may be related with modifications 
on the type classes mechanism that were added in Coq 8.4.  But I am not the 
right person to give a perfect clear answer about that!

Best regards,
        David.