The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

Hello Daniel,

On 08/25/2012 08:23 AM, Daniel de Rauglaudre wrote:
> 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 *)
You can use [Tactic Notation] to do this.

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

  Goal True -> 1 = 1 -> 2 = 2 -> True.
  intros H1 H2 H3.
  fast_omega H1 H2.

See also

  http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual015.html#toc84

> (BTW, is there a better way to accelerate omega?)
There is also a variant of omega, called romega, that is implemented by 
reflection.

Robbert