coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] matching variables in Ltac

From: Paolo Herms <paolo.herms AT cea.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] matching variables in Ltac
Date: Wed, 5 May 2010 12:09:56 +0200

Hello,

On Wednesday 05 May 2010 11:49:30 Loic Pottier wrote:
> with Ltac, can we match names of variables in a pattern, to use them in
> right-hand side? e.g:
>
Try this:
match goal with |- forall x:?E, @?P x => idtac x E P end.

Regards,
--
Paolo Herms
PhD Student - CEA-LIST Software Safety Lab. / INRIA ProVal Project
Paris, France

[Coq-Club] matching variables in Ltac, Loic Pottier
- Re: [Coq-Club] matching variables in Ltac, Paolo Herms
- Re: [Coq-Club] matching variables in Ltac, AUGER
- <Possible follow-ups>
- Re: [Coq-Club] matching variables in Ltac, Arthur Chargu�raud