Port stacking pass to Coq

This is a first attempt towards extracting the "backend" from Coq.

See src/coq/README.md for an overview.

Only the "stacking" pass is extracted. The "co_de_bruijn" stage is moved into Coq, and the stacking pass (in Coq) emits Micheline directly.

I ended up partly generalizing the codebase over the "location" type of the Michelson. Previously we used int locations, supplying dummy values when required. In this change, the Coq development is generalized over the location type, and some OCaml code is too. Some code now uses Location.t, so that the original source locations can be passed through to Michelson. (That will be useful later for unrelated things.) The location propagation into Michelson is not complete yet, but is not used for anything yet either.

I didn't want to handle record update in the Coq stage, so I just translated it away (to PAIR/CAR/CDR) for now. We could add it back someday if necessary. So far the new approach seems to be usually better in actual contracts, but maybe it is worse in some contracts...