The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Thu, Mar 19, 2009 at 08:35:29PM +0100, Pierre Corbineau wrote:
> 
> in the second case :
> 
> The problem has to do with the automation used (the congruence tactic 
> doesn't rewrite in match...with).
> 
> a workaround :

Thanks, that worked.

Is this a fundamental problem, or will it be fixed (so that the
workaround is not needed) in a future release?

Would I have more luck if I used the development version of coq?


Thanks
Ian