The Coq mailing list

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

Hi,

I'm having difficulty with the description of the tactic language in
https://coq.inria.fr/distrib/current/refman/proof-engine/ltac.html,
regarding goal selectors

Currently I have two subgoals, and a tactic called solve_eqs defined 
using Ltac.

At the present point,

repeat (2 : solve_eqs).
gives the message Syntax error: ')' expected after
[tactic:tactic_expr] (in [tactic:tactic_expr]).

repeat (only 2 : solve_eqs).
has no effect

2 : solve_eqs.
solves goal 2

After backing over this (ie we're looking at two unsolved goals)

the following two attempts give the same syntax error message as above.
repeat (only 1 : solve_eqs || only 2 : solve_eqs).
repeat (1 : solve_eqs || 2 : solve_eqs).

repeat ((only 1 : solve_eqs) || (only 2 : solve_eqs)).
gives Error: No such goal.

The following two just do nothing
repeat (only 1-2 : solve_eqs).
repeat (only 1-2 : try solve_eqs).

(and, by the way,
1: solve_eqs. does nothing, but
2 : solve_eqs. 1 : solve_eqs. solves both goals)

how 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?

Thanks

Jeremy