diff options
| author | Brian Campbell | 2019-02-14 17:09:58 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-02-15 18:17:42 +0000 |
| commit | 18b38f6495ea8836f332e9b5da8525caac338e28 (patch) | |
| tree | 5c9450f364fe31466de5e647f49af47e9bd033ec /src/scattered.ml | |
| parent | 65599f14b3ecac193529caafbee7672b38ed367e (diff) | |
Coq: Partial simplification of rich bool types
This uses the SMT solver to spot rich `atom_bool` types which don't contain
any information, replaces them with bool, and handles most of the
construction and projection of them.
The SMT part will be replaced by a simplification procedure soon, because
it can't handle some important cases.
Diffstat (limited to 'src/scattered.ml')
0 files changed, 0 insertions, 0 deletions