As suggested in #282, it can be useful to #ifdef code depending on
specific versions of CompCert.

Assuming a version number of the form MM.mm or MM.mm.pp
the following macros are predefined:

__COMPCERT_MAJOR__=MM       (the major version number)
__COMPCERT_MAJOR__=mm       (the minor version number)
__COMPCERT_PATCHLEVEL__=pp  (the patchlevel, or 0 if none)
__COMPCERT_VERSION__=MMmmpp (two decimal digits each, e.g. 30500 for version 3.5)

Major and minor numbers are enough, we don't need a patchlevel.
As a consequence __COMPCERT_VERSION__ is 305, not 30500, for version 3.05.