Primitive machine signed integers for Coq


An important issue for the use of Coq in industrial developments is its treatment of natural numbers and integers. As a mathematical programming language, Coq defines these numbers in a way that is useful to prove theorems about them, but is too inefficient to use in practical executions. To solve this problem, recently Coq introduced the Int63 type, which gives efficient machine unsigned integers available inside Coq. However, signed integers continued being unavailable, so the \textit{Prometheuss - Proof Methods for European Software Systems} team contributed them to Coq. They are called Sint63 and are now part of the latest Coq development branch, and will be part of the next official release of a Coq version.