The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT polytechnique.org>]

Is "change" supposed to work with pattern variables ? That'd be nice
but, unless it's been changed in the trunk, I don't see any reference
to it in the manual.
I just tested it on some examples and it seems to work (mostly), but
I'm wondering why it isn't explicitely said in Section 8.3.12 that
variables are supported. Maybe it's an experimental feature ?
In any case, what's true is that it shouldnt fail with a Not_found exception 
:)

S.

On Mon, Jul 11, 2011 at 11:54 AM, Paolo Herms 
<paolo.herms AT cea.fr>
 wrote:
> On Monday 11 July 2011 11:28:51 Coq Dev wrote:
>> Is it possible to fold a "not" after it has been unfolded? For instance:
>>
> And the following should work, too, but currently fails with an exception:
>
> change (?X -> False) with (not X) in *.
>
> Maybe anybody wants to fix this for a future version...
> --
> Paolo Herms
> PhD Student - CEA Software Safety Lab. / INRIA ProVal Project
> Paris, France
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06