coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jonathan <jonikelee AT gmail.com>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] difficulty computing with integers in Ltac
- Date: Mon, 01 Dec 2014 21:52:57 -0500
On 12/01/2014 06:12 PM, Jason Gross wrote:
...
Alternatively, you can write an ocaml plugin to convert a constr to an
int_or_var.
What is the best way to get started writing plugins? Is there a tutorial?
-- Jonathan
- [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/01/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Cedric Auger, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jason Gross, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- RE: [Coq-Club] difficulty computing with integers in Ltac, Georges Gonthier, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Hugo Herbelin, 12/03/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Pierre-Marie Pédrot, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Gregory Malecha, 12/02/2014
- RE: [Coq-Club] difficulty computing with integers in Ltac, Georges Gonthier, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Frédéric Besson, 12/02/2014
- Re: [Coq-Club] difficulty computing with integers in Ltac, Jonathan, 12/02/2014
Archive powered by MHonArc 2.6.18.