diff options
| author | Brian Campbell | 2019-08-02 11:39:25 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-08-02 11:39:25 +0100 |
| commit | 94e2f401263c7efc69f7d2b731827dc41bd8c1b8 (patch) | |
| tree | 7a6b0d46256c759c7ac2c4079d320d36267aa6a3 /src/pattern_completeness.ml | |
| parent | 8f9aa39623699f5b50f7abf6dc3c124062542b7e (diff) | |
Fix up some edge cases with the bitvector/polyvector split
Mostly in the Coq backend, plus a few testcases that use bitvector
builtins on poly-vectors (which works on some backends, but not Coq).
Also handle some additional list inclusion proofs in Coq.
Diffstat (limited to 'src/pattern_completeness.ml')
0 files changed, 0 insertions, 0 deletions