The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On 2011-02-09, Tom Prince wrote:
> Goal rec.
> (* I would think the following would also work, but "constuctor" seems
>    to be ignoring its argument. Anyway, I have a number of theorems that
>    can be proved like this that I would like automate. *)

I filled a bug about this (with a patch)
http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2496

> Ltac TAC k := (let n:= fresh "n" in (evar (n:nat); assert (Laws n) as P; 
> subst n); [ constructor k | apply (appl P) ]).
> constructor; [TAC 1 | TAC 3 | TAC 2].

With the patch, I can do

Tactic Notation "TAC" int_or_var(k) := (let n:= fresh "n" in (evar (n:Equal); 
assert (Laws n) as P; subst n); [ constructor k | apply (laws_true P) ]).
constructor; [TAC 1 | TAC 2].

But when I try to automate this:

Tactic Notation "TAC" int_or_var(k) := (let n:= fresh "n" in (evar (n:Equal); 
assert (Laws n) as P; subst n); [ constructor k | apply (laws_true P) ]).
Ltac do_with_nat n :=
 match n with 0 => TAC n | S ?n' => TAC n' || do_nat n' end.
constructor; do_nat 2.

it fails. It seems to be that it is impossible to do anything with
numbers destined to be used as tactic arguments, other than pass them
around.

  Tom