diff options
| author | Brian Campbell | 2018-07-18 11:35:04 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-07-18 11:35:04 +0100 |
| commit | 92f1e32b677d3b80eb509ddadb323714de2b3092 (patch) | |
| tree | 7db0d35da1e0f44da74a7f456bfe752f9fea5fc7 /src/monomorphise.ml | |
| parent | 0c5ff0aa6cd611ab40233b284b0a6054bc27166e (diff) | |
Coq: constraint solving improvements
Use eauto so that user-added hints are more flexible,
example with Replicate in aarch64, dropped zbool to prevent slow
proof searches (and preprocessing deals with boolean comparisons now).
Report failed constraints after preprocessing;
Separate preprocessing tactic out.
Diffstat (limited to 'src/monomorphise.ml')
0 files changed, 0 insertions, 0 deletions