The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Gergely,

SF defines its own nats in a module NatPlayground and then closes this 
module, so that the standard library nats are used. They do the same trick 
several times to just explain how things are done but then go back to the 
library definitions.

The nat notation is pretty hard wired into Coq. In Init.Datatypes at the 
beginning you find:

Declare ML Module "nat_syntax_plugin".

(note: this is not shown in the HTML dumps of the library sources, you need 
to look into the .v file). Afaik this does the trick. I can't tell how the 
nat type is actually connected to this plugin, I think it is simply hard 
wired by name in the plugin.

I guess this is nothing the Coq community is especially proud of, but it did 
work so far ...

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928