coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Developing Coq tactics

From: Sean Wilson <sean.wilson AT ed.ac.uk>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Developing Coq tactics
Date: Wed, 20 Jun 2007 17:10:37 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Organization: School of Informatics, The University of Edinburgh

Hi,

I'm interested in writing Coq tactics at the OCaml level but I'm having
trouble finding documentation to help me. I found this guide for an older
version of Coq:
http://www.iist.unu.edu/~alumni/software/other/inria/www/coq/doc/node.2.1.0.html

I have heard that Coq has changed a lot since then so I am looking for more
up-to-date documentation. Is there any useful documentation available?

Regards,

Sean

[Coq-Club] Developing Coq tactics, Sean Wilson