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 /test | |
| 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 'test')
| -rw-r--r-- | test/coq/skip | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/test/coq/skip b/test/coq/skip index e0096643..569774f4 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -12,4 +12,10 @@ pure_record.sail pure_record2.sail pure_record3.sail vector_access_dec.sail -vector_access.sail
\ No newline at end of file +vector_access.sail +XXXXX unsupported existential quantification of a vector length +bind_typ_var.sail +XXXXX needs impliciation in constraints fixed +bool_constraint.sail +XXXXX needs some smart existential instantiation +complex_exist_sat.sail |