| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
| |
- can now take learned clauses as argument
- returns a whole clause (and not only a literal)
- tested for the vernacular commands
Warning: seems to slow down 8.5 version
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
- Correct equality check of atoms and formulas for processing congruence closure
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
various solvers separately
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
(the last element is the default)
|
| |
|
| |
|
| |
|
|
|
|
| |
standard coq
|
| |
|
| |
|
|
|