The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 02/16/2015 05:26 AM, Pierre-Marie Pédrot wrote:
> On 16/02/2015 10:57, Pierre-Marie Pédrot wrote:
> > I am fairly sure that a ten-line plugin is enough to define the tactic
> > you're longing for.
> There you go.
>
> https://github.com/ppedrot/issection-tactic/tree/master
>
> PMP

Thanks, PMP!

OK - so this tactic was so easy to write in ML because there already was 
an "is_section_variable" function in ML... sigh...

I continue to be embarrassed by my lack of knowledge of how to write ML 
plugins for tactics.

But, is anyone going to create suitable documentation/tutorials on 
tactic plugin development to help?  For example, this plugin uses "match 
kind c with", while the closely related "is_var" tactic uses "match 
kind_of_term x with" - why the difference?

Beyond the lack of doc, my further reluctance is due to: whatever tactic 
I write with Ltac, as kludgey as it may be, it isn't going to cause 
problems for Coq after it executes.  Although I'm not sure about it, it 
seems to me that the same degree of safety isn't the case with ML tactic 
plugins.  Also, anything written in Ltac is insulated from internal 
changes in Coq (at least up to behavior changes in builtin Ltac tactics).

-- Jonathan