aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Compiles with Coq-8.10Chantal Keller2020-03-3111-113/+184
|
* Port to coq-8.10 under progressChantal Keller2020-03-3113-2720/+71
|
* Best practice on hintsChantal Keller2020-01-281-0/+8
|
* Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2020-01-282-79/+109
|\
| * Best practiceChantal Keller2020-01-281-0/+17
| |
| * Comments for conversion tacticsChantal Keller2020-01-211-79/+92
| |
* | Hint DB for QInstChantal Keller2020-01-281-1/+1
| |
* | Hints in databasesChantal Keller2020-01-2812-506/+481
| |
* | Towards coqppChantal Keller2020-01-161-35/+35
| |
* | ml4 -> mlgChantal Keller2020-01-164-4/+4
|/
* Use smt in the group exampleChantal Keller2020-01-161-9/+9
|
* Fix CI manifestChantal Keller2020-01-161-1/+4
|
* Add the full example of the webpage in the unit testsChantal Keller2020-01-161-0/+30
|
* Corrected the example on the webpage (fixes #56)Chantal Keller2020-01-161-11/+15
|
* A bit of CIChantal Keller2020-01-151-0/+44
|
* Correct linksChantal Keller2020-01-151-2/+2
|
* WebpageChantal Keller2020-01-151-1/+3
|
* Merge branch 'master' of github.com:smtcoq/smtcoqChantal Keller2020-01-153-9/+10
|\
| * Set theme jekyll-theme-slateckeller2020-01-151-0/+1
| |
| * Changing notation for implb (closes #51)Chantal Keller2019-11-142-9/+9
| |
* | More succinct READMEChantal Keller2020-01-152-270/+328
|/
* Update gitignoreChantal Keller2019-10-011-3/+5
|
* Open participationChantal Keller2019-09-261-14/+22
|
* TypoChantal Keller2019-09-251-0/+1
|
* TypoChantal Keller2019-09-251-1/+0
|
* An opam package is back!Chantal Keller2019-09-251-17/+18
|
* Top-level MakefileChantal Keller2019-09-251-0/+5
|
* Missing filesChantal Keller2019-09-252-0/+60
|
* Made SmtCommands independent from VeritSyntaxChantal Keller2019-09-2521-298/+240
| | | | Made lfsc/* mostly independent from VeritSyntax
* Remove unused fileChantal Keller2019-09-201-65/+0
|
* 3rdpartyChantal Keller2019-07-1511-35/+106
|
* DocumentationChantal Keller2019-04-121-3/+4
|
* DocumentationChantal Keller2019-04-122-4/+10
|
* Separate unit tests into vernac and tacticsChantal Keller2019-04-129-545/+587
|
* DocumentationChantal Keller2019-04-122-94/+119
|
* Properly check veriT exit code and warnings (#48)ckeller2019-04-125-9/+17
| | | * Report veriT warnings
* Error message to state that tactics are not supported with native-coq (#47)ckeller2019-04-129-65/+149
| | | * Better error message for failing tactics with native-coq
* Check again that veriT returns a zero exit codeChantal Keller2019-04-121-1/+1
|
* Remove check of veriT non-zero exit codeChantal Keller2019-04-101-1/+1
|
* More uniformity in INSTALLChantal Keller2019-03-151-10/+12
|
* Use CVC4 version 1.6Chantal Keller2019-03-151-6/+10
|
* Tactics are broken with native-coq (fixes #38)Chantal Keller2019-03-151-7/+12
|
* Explain LFSCSIGS in the installation instructions for CVC4Chantal Keller2019-03-151-21/+17
|
* V8.9 (#43)ckeller2019-03-1519-57/+2746
| | | | | | | | | | | | | | | | | | | | * 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
* Support for native-coqChantal Keller2019-03-122-9/+14
|
* Switch to 8.8 in INSTALL.mdChantal Keller2019-03-121-11/+11
|
* V8.8 (#42)ckeller2019-03-1134-1063/+1146
| | | | | | | | | | | | | | | | | | | | * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Organization structures * 8.8 ok with standard coq
* No hard-coded paths to executables (fixes #37)Chantal Keller2019-03-054-889/+6
|
* int does not exist in standard coqValentin Blot2019-02-281-4/+1
|
* Re-fixes in Example.vValentin Blot2019-02-281-3/+4
|
generated by cgit (git 2.34.1) at 2024-07-03 15:09:47 +0000