The Coq mailing list

[Bradford Larsen <brad.larsen AT gmail.com>]

I want to modify `eauto` and provide it as a new tactic.  I've been
able to successfully modify and use the `eauto` tactic in the Coq
source distribution, but I'd like to be able to build my modified
version separately as a plugin, without needing to modify the Coq
distribution.

I'm looking for an example of a separately distributed tactic written
in OCaml.  The Coq FAQ says, "You have some examples of tactics
written in Ocaml in the “contrib” directory of Coq sources"
<http://coq.inria.fr/faq?som=11#htoc154>.  Unfortunately, there is no
`contrib` directory to be found.

Does anyone have an example of a separately distributed tactic written
in OCaml?  (I'm particularly interested in the makefile for such a
plugin.)

Thanks,
Brad Larsen