summaryrefslogtreecommitdiff
path: root/src/rewrites.mli
diff options
context:
space:
mode:
authorBrian Campbell2019-03-15 18:42:00 +0000
committerBrian Campbell2019-03-15 18:42:09 +0000
commit11325d9bb5f4117c5b41413ac523b7d50577ebdd (patch)
treeff7bdf38eb6b3b0d2665badac4ac3287629cc188 /src/rewrites.mli
parentc1f9e24213b50fb622ac94f816e304eabc75ba75 (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/rewrites.mli')
0 files changed, 0 insertions, 0 deletions