coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] C-zar proof help

From: Taral <taralx AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] C-zar proof help
Date: Thu, 19 Mar 2009 17:54:59 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :content-type:content-transfer-encoding; b=jyr+ZQBlzAy7l8r1sGQH7eqyeW1BKUr7p9zRTZ7BNT0lOSk4pN8T8pwybBhAyAzEuq J5cQzvwd1FvEFM9wtS8Dhs8qULWqdA3GvVawelvpZ3nE2cAKPUz8vRX1VdJjqdL1GUve VLxvI41aNo5G7DA5qF3oPlhLFLhLa1/gkoqW4=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On Thu, Mar 19, 2009 at 12:35 PM, Pierre Corbineau
<pierre.corbineau AT laposte.net>
wrote:
> The problem has to do with the automation used (the congruence tactic
> doesn't rewrite in match...with).

Is that fixable or would it break the tactic?

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
-- Unknown

Re: [Coq-Club] C-zar proof help, (continued)