| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
This is a revised version of #62 with a workaround for coq/coq#12603.
closes #62
|
|
|
|
|
|
|
| |
* Add a test target for asynchronous proof checking (does not fully reflect the coqide behavior though)
* Make the selected lemmas persistant
Co-authored-by: Chantal Keller <Chantal.Keller@lri.fr>
|
| |
|
|
|
| |
This reverts commit dfbf0a5674ae1ab0dc68c15ae4b5df8cc439b741.
|
|
|
|
| |
We fix the way SMTCoq searches for the num library, both when building
and when generating .merlin.
|
| |
|
| |
|
|
* 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
|