coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about documentation of Coq implementation

From: "Yamamoto, Yosuke" <yoy553 AT mail.usask.ca>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Question about documentation of Coq implementation
Date: Tue, 09 Sep 2014 17:12:14 +0000
Accept-language: en-US

Hi,

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?

Yosuke

[Coq-Club] Question about documentation of Coq implementation, Yamamoto, Yosuke, 09/09/2014
- Re: [Coq-Club] Question about documentation of Coq implementation, Pierre-Marie Pédrot, 09/10/2014
  - Re: [Coq-Club] Question about documentation of Coq implementation, Yosuke Yamamoto, 09/10/2014