Global integer constants should be translated to their value

[tchajed]

Rather than translate const declarations to global expressions, we should try to translate them to their value in Z and then use them as #ConstName. We would probably not bother emitting an expression in the source code (instead using the Go API to evaluate compile-time constants), but the benefits are:

• We can support infinite-precision constants, which are the easiest to write down.
• Coq proofs can directly use constants from the code rather than separate ones.