sail/test/coq/pass, branch sail2

Coq: remove last use and definition of doc_nc_prop

2019-12-01T21:34:23+00:00

(plus test, as it wasn't covered before)

Coq: limited support for existentially-typed tuples

2019-10-02T10:40:38+00:00

- 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)

Enable part of a test that's been fixed recently.

2019-09-02T16:04:09+00:00

Add a couple of overlooked tests

2019-08-30T13:38:29+00:00

Coq: add missing property derivation casts for effectful expressions

2019-06-21T13:44:29+00:00

These don't appear much, but are now showing up in the sail-arm model
due to an innocent change elsewhere.

Coq: be more careful when dealing with wildcard argument patterns

2019-06-21T09:57:15+00:00

If they're merged with a type variable then we still need to name the
argument so that it can be used in other types.

Test case for previous commit

2019-06-03T17:31:53+00:00

Coq: support if-then-throw typechecking special case

2019-05-24T15:08:14+00:00

Coq: introduce autocasts at variables

2019-05-21T10:56:46+00:00

Usually we do this at function applications and casts, but occasionally
a variable is used at a different type.

Coq: support pure loops with termination measures

2019-04-17T17:30:49+00:00