coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re : Folding 'not'

From: Coq Dev <coqletsgo AT yahoo.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Re : Folding 'not'
Date: Fri, 22 Jul 2011 13:51:00 +0100 (BST)
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=X-YMail-OSG:Received:X-Mailer:References:Message-ID:Date:From:Subject:To:In-Reply-To:MIME-Version:Content-Type; b=KbfStwk5jcrbidj4/hWSDdntsyVG97QQDvYZhXPXMQDqIfua/q6Z5W/79DncGtTDoOw1XQ71StjOjYLVeYE/cBXcQm2dTBjAS2PnomnoTFyZBJqHDTpg73p7UF7nMxToaiB16w1poedY7g8jiAC0ApntcW9WjusNzcUcwrhCKnE=;

I'm sorry, this is a little too late to realize it, but apparently my wish has already been granted: the CHANGES file of Coq 8.3 states that:

Changes from V8.2 to V8.3
=========================

- Tactic "intuition" now preserves inner "iff" and "not" (exceptional
source of incompatibilities solvable by redefining "intuition" as
"unfold iff, not in *; intuition", or by using "Set Intuition Unfolding".)

However, I tried "Set Intuition Unfolding" but I got "Warning: There is no option Intuition Unfolding." both in Coq 8.3pl1 and 8.3pl2 without success. I'll report it as a bug.

Thanks anyway for everyone's help, I learned quite some tricks and things about Ltac.

[Coq-Club] Folding 'not', Coq Dev
- Re: [Coq-Club] Folding 'not', gallais @ ensl.org
- Re: [Coq-Club] Folding 'not', St�phane Lescuyer
- [Coq-Club] Re : Folding 'not', Coq Dev
  - [Coq-Club] Re : Folding 'not', Coq Dev
- <Possible follow-ups>
- Re: [Coq-Club] Folding 'not', Paolo Herms
  - Re: [Coq-Club] Folding 'not', St�phane Lescuyer