The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

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.

-- 
Regards
Christian