The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Hi,

I am interested in adding my own top-level declaration forms, like “Program 
Definition” and “Functional Scheme”, which generate obligations and/or add 
definitions to the current section / module. Is there any documentation on 
how to do this? Presumably, I could define such a thing as a separate ML 
module that could be loaded into Coq, without modifying the Coq source 
itself. I have been looking a little at the plugins/ directory for some 
examples, but it would be much easier to wade through that code with a little 
bit of guidance.

Thanks,
-Eddy