The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

Hello,

Is there some way to declare my own custom interpretation of integer 
constants in a scope, as are available in the nat and Z scopes?  If I have 
a function Z_to_foo : Z -> foo, I'd like to be able to make, for instance, 
"4" automatically intepreted as "Z_to_foo 4" in a particular context.  I 
looked around on the manual and the nat and Z libraries but couldn't find 
anything.  Coercions sort of do what I want, but it doesn't seem like you 
can tie them to particular notation scopes.  Or is this how nat and Z do 
it?  Thanks!

-Andrew