The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 12 janv. 10 à 09:31, Christian Doczkal a écrit :

> Hello
>
> > A couple years back I started writing a Howto on ML level  
> > customization.
> > It is now available on
> >
> > http://coq.inria.fr/cocorico/CoqCustomizationHowTo
> >
> > It is very incomplete and may be somewhat out of date but may provide
> > some help.
>
> Yes, thank you for pointing me to it. The part about having to enter  
> ml4
> files no langer applies, but the rest allowed me to finally have a
> compiling starting point.
>
> Unfortunately thats where the tutorial stops. Since there seems to be
> next to no other documentation on how to write tactics at the ML  
> level,
> it would be great if this could be extended.

Hi Christian,

  I made an example plugin with a small tactic that gives you the
list of constructors of an inductive type in a list. It's documented and
covers the basics of making a plugin and a small tactic extension.

http://github.com/mattam82/Constructors

Hope this helps,
-- Matthieu