diff options
| author | Brian Campbell | 2019-12-09 16:11:09 +0000 |
|---|---|---|
| committer | Brian Campbell | 2019-12-09 16:11:09 +0000 |
| commit | 1aeb3db72e08a463e04632992ca3bd668ee4e52e (patch) | |
| tree | 67f6a36ce625fd81b7055ebc6c3a94f60b2b41ea /x86/x86_extras_embed_sequential.lem | |
| parent | 235a320e94b432c3ccf021d77c6e8303e1d1a19d (diff) | |
Coq: improve solver enough to handle arm spec
- break up goals more in unbool
- remove intuition from guess_ex_solver because it can be too expensive
- flip goals around because the side that evars appears on has changed
- generalise the and/or tactics
- make a couple of tactics more specific/robust
Diffstat (limited to 'x86/x86_extras_embed_sequential.lem')
0 files changed, 0 insertions, 0 deletions