The Coq mailing list

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

On 09/09/2014 19:12, Yamamoto, Yosuke wrote:
> I am looking for a documentation of Coq implementation. I found the
> chapter “Writing ad-hoc Tactics in Coq” of an old Coq manual (ver6.3.1)
> has a brief description but seems outdated. Is there a thorough
> description of Coq implmenetation available, like the chapter “A
> Tactical Theorem Prover” of a book “ML for the working programmer” for LCF?

There is partially outdated documentation in the dev/doc folder of Coq
sources. Apart from that, I think you'll need to dive in the code
yourself. What do you want to do exactly? Writing ML tactics?

PMP

Attachment: signature.asc
Description: OpenPGP digital signature