coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac & variable # of parameters

From: Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac & variable # of parameters
Date: Sat, 25 Aug 2012 19:24:15 +0200

Hi,

On Sat, Aug 25, 2012 at 12:07:52PM +0200, Robbert Krebbers wrote:

> Tactic Notation "fast_omega" hyp_list(Hs) :=
> revert Hs; clear; idtac "do omega".

Thanks. That does the job.

--
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/

[Coq-Club] Ltac & variable # of parameters, Daniel de Rauglaudre, 08/25/2012
- Re: [Coq-Club] Ltac & variable # of parameters, Robbert Krebbers, 08/25/2012
  - Re: [Coq-Club] Ltac & variable # of parameters, Laurent Théry, 08/25/2012
  - Re: [Coq-Club] Ltac & variable # of parameters, Daniel de Rauglaudre, 08/25/2012