diff options
| author | Brian Campbell | 2019-03-15 18:42:00 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-15 18:42:09 +0000 |
| commit | 11325d9bb5f4117c5b41413ac523b7d50577ebdd (patch) | |
| tree | ff7bdf38eb6b3b0d2665badac4ac3287629cc188 /src/initial_check.mli | |
| parent | c1f9e24213b50fb622ac94f816e304eabc75ba75 (diff) | |
Coq: some progress on the test suite
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.
Diffstat (limited to 'src/initial_check.mli')
0 files changed, 0 insertions, 0 deletions