| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
* The tactics sets veritXXX and smtXXX now automatically take hypotheses from the local context
* `prop2bool_hyps` also apply to hypotheses not in the local context
* Second strategy for vauto (still incomplete)
|
|
|
|
|
|
|
| |
* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed.
* Some current limitations are detailed in src/PropToBool.v.
* Partially enhances #30 .
|
|
|
|
|
| |
Equality is now treated from uninterpreted sorts, which makes them usable with tactics!
Closes #17
Closes #78
|
|
* Better error message for failing tactics with native-coq
|