Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] difficulty computing with integers in Ltac

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] difficulty computing with integers in Ltac


Chronological Thread 
  • From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] difficulty computing with integers in Ltac
  • Date: Tue, 02 Dec 2014 14:19:17 +0100

On 02/12/2014 03:52, Jonathan wrote:
> What is the best way to get started writing plugins? Is there a tutorial?

There was a blog post at Gallium.

http://gallium.inria.fr/blog/your-first-coq-plugin/

It is a bit outdated w.r.t. to trunk though. When I have time, I should
write one too, but this is not really to happen soon...

PMP


Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page