Error messaging capability in Coq mode

Modify Coq-MenhirLib to return information about the parser state and token when the error occurred and modify the generated parser to include a nat_of_state function to add in the use of this information.

Providing some meaningful data to the callee when the parser fails allows them to construct error messages from the verified parser only. If the tokens (as they do in CompCert and many other parsers) include location information, that can be retrieved. To aid in the usage of the state in these messages, I added a small function to the generated parser automata that maps from states to their number. This enables the use of the existing .messages file format and the code Menhir already generates.

This MR also updates the manual in /doc and adds a demo calc-syntax-errors in the style of coq-minicalc and calc-syntax-errors.

This is not a breaking change for any users of the Coq code due to the addition of the annotation synonym for the new return information, but extracted code will need to be updated to ignore this information if they do not desire to use it.