The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  If you really need this particular feature, you might want to consider the 
Ssreflect plugin. Ssreflect tactics generally accept Coq integers along Caml 
ones; in particular it is possible to compute iteration counts (as in do 
N!tactic), occurrence selectors (set x := {+N}y), and subgoal selectors 
(tac1; first N [tacN]).
 -- Georges

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Jonathan
Sent: 02 December 2014 02:53
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] difficulty computing with integers in Ltac

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