- rename files to get rid of prefix
- use -Q to get package name right
- add Base.v to make package imports simpler
- add opam file for coq package

- in particular at monadic interfaces (i.e., sufficient for instruction
  ast types)
- see commented out part of test/coq/pass/ast_with_dep_tuple.sail for an
  example that's not currently supported
- generate definitions for type-level Bool definitions (i.e., predicates)

Currently only supports pure termination measures for loops with effects.

The user syntax uses separate termination measure declarations, as in the
previous recursive termination measures, which are rewritten into the
loop AST nodes before type checking (because it would be rather difficult
to calculate the correct environment to type check the separate declaration
in).

- add dummy print_bits function
- support int(1) like types in axioms

- skip a few more that aren't supported yet
- produce better debugging information (in particular, in the right order)
- avoid some autocasts that aren't supported yet and are usually
  unnecessary
- Handle more constraints like `8 * n = 8 * ?Goal`

Rewrite <> true/false in goals.
Correct implicits in record and variant types.
Use expanded valspecs from the type checker in axioms.
Allow list notations in type definitions.
Skip some not-yet-supported tests.