The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi everybody,
I want to define a tactic which repeats a command a number 'n' of 
times(both the command and the number are given in arguments)
I tried several ways but no one succeeded...
The first solution using Ltac langage is to use the tactical  (do num 
expr...)
Unfortunately  it doesn't work because do expects a natural number and 
'a priori' we don't know the type of the argument n:

(**********v8 syntax  :-) ************)
Ltac repeatTac n expTac:= do n expTac.
(**********************************)

This definition generates a syntax error as I said before...

Another solution is to define a recursive tactic as follows:
(*****************************)
Ltac repeatTacRec n expTac :=
match eval compute in  n with
| [0%N] => idtac
| _ => expTac; repeatTacRec (pred n) expTac
end.
(*****************************)
The second solution compiles without any difficulties but I 'm  unable 
to use it :
Example:
(************************)
Definition toto:forall (a:nat) , a=a .
(*************************)
In this simple example 'repeatTacRec 1%N auto'  should solve the goal 
...but this is not the case !
Thanks for helping me to understand what's the matter!!

Houda ANOUN
LaBRI