The Coq mailing list

[Épiphanie <landeguy AT gmail.com>]

> 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

> A few other plugins that I have written might help
> - template-coq (https://github.com/gmalecha/template-coq) constructs a 
> syntactic representation of Coq terms within Coq.
> - coq-plugin-utils (https://github.com/gmalecha/coq-plugin-utils) has 
> a few functions that I have found useful when writing Coq plugins, 
> particularly ones that extend Ltac.
>
> Thomas Braibant also wrote a timing plugin that is documented. I'm not 
> certain if it is still compatible with 8.5
> https://github.com/braibant/Timing-plugin


Thanks Gregory for all those links, I will definitely take a close look 
at this, and try to learn from the source.
I'm just surprised there is no official documentation for this though.
Well, I shall try to write my own plugin then :think:

Thanks to both of you for your help so far!