The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

OK, well, no doubt I didn't try for quite the right way of expressing it 
but surely being misled on this point wouldn't lead to syntax errors, 
would it?

How do I correctly write the tactic I tried to write as
repeat (only 1 : solve_eqs || only 2 : solve_eqs).

And what should
repeat (only 2 : solve_eqs).
do?  I'm guessing that it means the second and subsequent invocations of
apply to the second subgoal produced by the previous invocation of 
solve_eqs, but that doesn't explain why nothing happens on the first 
invocation.

And what should
repeat (only 1-2 : try solve_eqs).
do?  Again, shouldn't the first invocation of
only 1-2 : try solve_eqs
apply solve_eqs to each of the two subgoals?

Anyway, what I would like to know how to do is to apply a tactic 
repeatedly to all the goals in turn, until they are all solved or there 
is no further progress

Thanks,

Jeremy

On 01/24/2019 11:05 PM, Laurent Thery wrote:
> 
> 
> On 1/24/19 5:35 AM, Jeremy Dawson wrote:
>> ow do I write a tactic to repeatedly apply solve_eqs to goals 1 and 2
>> until either both are solved or there is no further progress?
> 
> Maybe you are mislead by the fact that the goal numbering is local but
> not global
> 
> For example:
> 
> Goal (True /\ True) /\ (False /\ True).
> split; only 2 : (split; only 2 : trivial).
> 
> solves the 3th goal
>