The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 10/11/2013 12:03 AM, t x wrote:
> Is there a way I can, using only a finite number of lines,  map ..., -3,
> -2, -1, 0, 1, 2, 3, ... to my own definition of Int?
> (or does this require delving down into the level of ocaml)
You can define a coercion from the integers Z to your own type (but I am 
not sure whether that always works well when combined with a notation 
scope for your own integer type).

Alternatively, you can use a plug-in written in Ocaml, see

  plugins/syntax/z_syntax.ml

in the Coq source tree for an example.