The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Hi friends,

Since omega is sometimes slow, I found a trick to accelerate it
sometimes. Suppose only hypothese Hr and Hp are necessary for
omega to work, I do:
     revert Hr Hp; clear; intros; omega

Good. Now, I would like to make a Ltac:
   Ltac fast_omega x y := revert x y; clear; intros; omega.

And I can write:
   fast_omega Hr Hp.

But how do I have a Ltac allowing me to use a variable number of
parameters (not just 2)? I would like to be able to write, depending
on the circumstances, e.g.:
   fast_omega.               (* clear; intros; omega *)
   fast_omega Hr Hp.         (* revert Hr Hp; clear; intros; omega *)
   fast_omega H₁ Heqb Haft.  (* revert H₁ Heqb Haft; clear; intros; omega *)

How do I program my ltac?

(BTW, is there a better way to accelerate omega?)

Thanks.

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