The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 12/10/2015 06:54 PM, Epiphanie wrote:
> ...
> Finally, I have questions about LTac. This language seems powerful enough
> to perform interesting automation, however as a post on Galinium showed,
> there seems to be some heavy restriction on it.
> For instance, I cannot find a way to use the Search mechanic (vernacular
> command) inside a tactic, or even to know the number of subgoal there is.

See: https://coq.inria.fr/bugs/show_bug.cgi?id=3945

> I skimmed through the code of SSReflect and they do it through caml plugin,
> just like the said post suggested.
> However, I found nothing in the documentation about how to write your own
> Coq extension just like SSReflect does, and its consacred section on the
> FAQ is left blank.

This is a source of continuous frustration and debate.

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.

Still, for many purposes, there seems to be little alternative but to 
write an OCaml plugin.  This appears to be because Ltac's ability to 
automate procedures is treated as very secondary to its direct 
interactive usage.  Even though the ability to easily automate complex 
procedures would of course improve that direct interactive usage.

-- Jonathan