| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| |
| |
| |
| |
| |
| |
| | |
* 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 .
|
| | |
|
|/ |
|
|
|
|
| |
Made lfsc/* mostly independent from VeritSyntax
|
| |
|
|
|
| |
* Better error message for failing tactics with native-coq
|
|
* New syntax for implicit arguments
* Towards 8.9: problems with Micromega plugin
* Move to _CoqProject
* Back to name Makefile
* Switch to Makefile.local instead of -extra
* The compilation issue is a Coq bug
* Ok with 8.9
* INSTALL with 8.9
* Everything ok with 8.9
|