coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Rewriting with Existentials

From: "Jonas B. Jensen" <jobr AT itu.dk>
To: Gregory Malecha <gmalecha AT eecs.harvard.edu>
Cc: Coq Club <coq-club AT inria.fr>, Jesper Bengtson <jebe AT itu.dk>
Subject: Re: [Coq-Club] Rewriting with Existentials
Date: Tue, 31 May 2011 10:07:59 +0200

On Tue, May 31, 2011 at 10:00, Jonas B. Jensen
<jobr AT itu.dk>
wrote:
> Ltac ugly_evar_hack_create :=
> �repeat (match goal with
> � � � � � �[ |- context[?x]] => is_evar x; let l := fresh "l" in
> remember x as l
> � � � � �end).

By the way, this only works on Coq 8.3pl1 and up.

[Coq-Club] Rewriting with Existentials, Gregory Malecha
- Re: [Coq-Club] Rewriting with Existentials, Jonas B. Jensen
  - Re: [Coq-Club] Rewriting with Existentials, Jonas B. Jensen