The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

On Fri, 07 Oct 2005 07:17:29 -0700 Adam Chlipala
<adamc AT cs.berkeley.edu>
 wrote:

> I've managed to decipher the relevant parts of the Coq source code
> well enough to implement a new tactic in OCaml.  However, I had to
> modify the Makefile and basically make it "built-in" to use it.
> Is there a better way for me to do things so that I can distribute my 
> tactic as a "plug-in"?

You should look at the documentation of the cokmktop tool, at the
"Building a toplevel extended with user tactics" section:

http://coq.inria.fr/doc/Reference-Manual015.html#toc77

The idea is that once you have compiled your files into cmo (resp. cmx),
you can build a new coqtop (resp. coqtop.opt) linked with this new cmo
(resp cmx). So you can distribute only your files, with a small
dedicated makefile which build the cmo/cmx (it must know where to
find coq source path, use the coq_makefile tool to build such a
makefile), and builds the new toplevel with cokmktop. 

Cheers,

Pierre