Use the ascii decider from the stdlib which is extracted correctly.
Use strings in Coq and support break/continue natively.

We now use strings for names of structs/unions, goto labels, and function
names in the Coq part. Also in the frontend, we use strings for all names.

This has the following advantages:
* No need to rename in the Ocaml part. This makes the code better readable.
* Given C syntax in Coq, we can see easily trace where names came from.
* We can generate better error messages (remains to be done).

But also some disadvantages:
* Maps/sets with string indexes are potentially slower. We have implemented
  these using uncompressed Patricia trees, so it is not super bad (and this
  gives at least canonical representations), but these trees can become
  rather big.
* Generating fresh strings is annoying, but we only used that to generate
  names for labels of gotos for break/continue. These are now natively
  supported in the semantics.

Break and continue is now natively supported in the C semantics. We have
introduced the constructs

  break n
  breakto s

The construct break n breaks to the nth surrounding breakto.