The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

AAC_tactics may suit your needs [1]. Otherwise, there is the
Constructors demo plugin by Matthieu Sozeau [2], which served as a
base for some OCaml plugins. Both these plugins will give you the kind
of Makefile you want (note that in the case of AAC_tactics, it was
require to heavily patch the Makefile generated by coq_makefile,
because the plugin is a bit more involved than Constructors), and both
should work with Coq 8.3. You may also want to have a look at [4].

Note that coq_makefile undergo some radical changes in the trunk,
which make useless  the patching in AAC_tactics, and simplifies the
generation of the Makefiles. An example of plugin that should work
with the trunk is located here [3]. (Note that this tutorial project
has not been updated in a while, and could benefit from more work, but
it may be useful for you.)

With best regards,
Thomas
[1] http://sardes.inrialpes.fr/~braibant/aac_tactics/
[2] https://github.com/mattam82/Constructors
[3] https://github.com/braibant/coq-tutorial-ml-tactics
[4] https://github.com/pilki/cases


On Thu, Sep 29, 2011 at 6:25 PM, Bradford Larsen 
<brad.larsen AT gmail.com>
 wrote:
> 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
>
>