In version.h, GMP_NUMB_BITS is needed only for mini-gmp builds. In
non-mini-gmp builds, substitute a dummy value there, to make the
contents of this header file platform independent. In Makefile, we
always need a properly configured value, and do this with the renamed
variable NUMB_BITS.