The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 12/12/2015 07:24 PM, Épiphanie wrote:
> > See: https://coq.inria.fr/bugs/show_bug.cgi?id=3945
> Oki, I'll post on this then.
> > Ltac is actually quite a bit more powerful than one might expect - 
> > than even its developers anticipated. For example, it is possible to 
> > write an Ltac tactic that can know the number of subgoals. It is even 
> > possible to write an Ltac tactic that can label the subgoals with 
> > their relative numbers.
> Could you show the syntax for this or a link I have missed? I checked 
> again the official tutorial, and 2 others that were fully detailed but 
> found nothing about this

To determine the number of goals, use the numgoals tactical available in 
Coq version 8.5.    For instance, in a proof, if you execute the 
following line:

  all: let n:=numgoals in idtac n.

Coq will print the number of subgoals in focus.  There is no easy way to 
do it prior to 8.5.

For actually labeling goals with their relative numbers, this requires a 
rather complex tactic containing several Ltac hacks, which I wrote once, 
but don't have immediately available.  If you really need this, I can 
try to find it.

-- Jonathan