The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 31 Oct 2011 18:40:41 +0100,
Valentin ROBERT 
<valentin.robert.42 AT gmail.com>
 a écrit :

> I actually use it a few times (not too many though), and Guillaume
> Gallais' answer definitely helped me.
> 
> Concerning "do num tac", I was probably wrong in its semantics as I
> acknowledged, I just thought I could use it to rewrite something like:
> 
> feed H; [..|feed H]; [..|feed H]; [..|feed H].

it is the case (excepted for the first "feed H;"), but it has the same
problem that you have with what you wanted to do:
...; [..|feed H]; [..|feed H].
        ^            ^
        |            |
        |         this is applied on each subgoal generated by
        +----------------------------------------------------+

> 
> I had actually tried to write the recursive tactic with a decreasing
> nat, but I was missing the proper syntax to do so.
> 
> Thanks to you both.
>