The Coq mailing list

[Pierre Letouzey <pierre.letouzey AT inria.fr>]

----- Mail original -----
> 
> 
> Dear coq-club,
> 
> I read in Ch.12 of the reference book that numeral notations are
> defined in OCaml level, not in the Coq level. That sounded very
> understandable to me.
> I wonder in which file the numerical notations are coded for nat,
> positive, Z, R, and Q. (I could not find a separate i.e.
> non-Coq-level numeral notation for Q, though.)
> 
> 
> HyungSun Kim

Hi

You should have a look at the plugins/syntax/ directory in the coq
sources. For instance plugins/syntax/nat_syntax.ml for nat...

Best regards
Pierre Letouzey