diff options
| author | Brian Campbell | 2019-03-19 11:41:31 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-03-19 11:41:31 +0000 |
| commit | 496e9cf4709318f304a312f99dad8264efc06bf5 (patch) | |
| tree | 27fbff783d9443fc73682ca5527540a712a20ca3 /test/coq | |
| parent | 675dbaf2634bfd21043484e97918ab537a563e86 (diff) | |
Coq: more work on tests
- 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`
Diffstat (limited to 'test/coq')
| -rw-r--r-- | test/coq/skip | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/coq/skip b/test/coq/skip index 569774f4..f224e5fa 100644 --- a/test/coq/skip +++ b/test/coq/skip @@ -19,3 +19,15 @@ XXXXX needs impliciation in constraints fixed bool_constraint.sail XXXXX needs some smart existential instantiation complex_exist_sat.sail +XXXXX needs name collision avoidance due to type/constructor punning +constraint_ctor.sail +XXXXX Complex existential type - probably going to need this for ARM instruction ASTs +execute_decode_hard.sail +existential_ast.sail +existential_ast2.sail +existential_ast3.sail +XXXXX Needs an existential witness +exist1.sail +exist2.sail +XXXXX Needs a type synonym expanded - awkward because we don't attach environments everywhere +exist_synonym.sail |