The Coq mailing list

[Pierre Corbineau <pierre.corbineau AT laposte.net>]

It is fixable. I'll try to make a fix before the summer. The C-zar code
is currently identical in 8.2 and trunk.

Pierre


Ian Lynagh a écrit :
> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club