The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

Note that repeat runs the inner tactic focused on each goal separately
so "repeat (all: solve_eqs)" would (if the syntax allowed it) be the 
same as "repeat (only 1: solve_eqs)" which is also the same as "repeat 
solve_eqs", and "repeat (only 2: solve_eqs)" is the same as "repeat 
fail" ie idtac.

I feel like "all: repeat solve_eqs" should work given what you describe, 
can you explain how it fails?

Gaëtan Gilbert

On 25/01/2019 06:54, Jeremy Dawson wrote:
> Hi Cyprian,
>
> What I wanted is what I would express as
> repeat (all : solve_eqs)
> but it seems as though that form is forbidden.
>
> The various things I tried as indicated in my earlier email were simply
> looking for alternatives that work.
>
> Detailed background to what I want: solve_eqs doesn't seem to enlarge
> the number of goals in the cases where I want to use it, and sometimes
> solves a goal, sometimes only after solve_eqs has instantiated an evar
> in another goal, sometimes only after being repeatedly called on the
> same goal (where each time it simplifies the goal)
>
> Cheers,
>
> Jeremy
>
>
> On 01/25/2019 10:00 AM, Cyprien Mangin wrote:
> > What you probably meant is something like "all : repeat solve_eqs"