[Coq backend] Surjection without matching on int31 literal

Currently, the Coq backend of Menhir generates Coq programs which include pattern matching on 31-bit machine integers. The patterns are written as literal values. These literal values are syntactic sugar for their binary decompositions (using the I31 constructor and the digits values D0 and D1). Thus internally, such pattern matching is represented as thirty-two nested matches (on the I31 box and then each digit).

This feature (using literal 31-bit values as patterns) may disappear in future versions of Coq (hopefully 8.10), when primitive (63-bit) machine integers are introduced.

Therefore, this PR removes the use of this feature in Coq programs produced by Menhir. The matching on the individual bits of the 31-bit machine integers is made explicit, and the opening of the I31 box is done through the int31_rect eliminator of the int31 data type.

The only noticeable change introduced by this PR is that the generated code is a bit more verbose: patterns use a binary representation instead of a decimal representation. The computational behavior of these surj functions should be preserved.