The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 20/10/2014 19:38, Eddy Westbrook wrote:
> 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.

For the definition of an extra command, you need to use the VERNAC
COMMAND EXTEND macro in a ml4 file. According to the version of Coq you
are using (i.e. up to 8.4 included vs. trunk), the exact syntax of this
macro differs. You should look at ml4 files containing such macros to
grasp the idea. The tactics/extratactics.ml4 file may be a good start.

For the adding definition part, it may be rather complicated, depending
on the precise use case you have in mind. Maybe you could share some
details on this list?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature