coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Roland Zumkeller <Roland.Zumkeller AT polytechnique.fr>
To: mulhern <mulhern AT gmail.com>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club]Applying reduction rules to generated proofs
Date: Tue, 25 Apr 2006 08:13:50 +0200
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:from:subject:date:to:x-mailer:sender; b=I/V1D8cLqY51aGbbYO5iA6BL55aKVyvyqASLODiCwWeLIiChAgCEakxC4zlO+dEt2hPpUMg2JMob2salqjuBZm3teL4UW8v+A3vkrzFQF57p7vdNWPiL7hYQ0AzKM3YSVrObmk+Eq+yOImfdjM6wfUdeZzhy75ykSlvTri3iGts=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

I think you are looking for
Eval cbv zeta delta[name] in name.

On Apr 25, 2006, at 3:08 AM, mulhern wrote:

My purpose in performing these reductions is to transform the proof to
one that is more readily accepted by the refine tactic.

Could you show us an example?

Hope this helps,

Roland

--
http://www.lix.polytechnique.fr/~zumkeller/

[Coq-Club]Applying reduction rules to generated proofs, mulhern
- Re: [Coq-Club]Applying reduction rules to generated proofs, Roland Zumkeller
- Re: [Coq-Club]Applying reduction rules to generated proofs, Pierre Courtieu
- [Coq-Club]Re: Applying reduction rules to generated proofs, mulhern