aboutsummaryrefslogtreecommitdiffstats
path: root/src/zchaff/zchaff.ml
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-171-1/+1
|\
| * Update copyrightChantal Keller2022-02-161-1/+1
* | Use the Register mechanism (#104)ckeller2022-02-151-24/+18
* | getting rid of native-coq (#95)vblot2021-05-281-58/+58
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-261-1/+1
|\|
| * Update copyrightChantal Keller2021-05-261-1/+1
* | Port to coq-8.10 under progressChantal Keller2020-03-311-1/+1
|/
* V8.8 (#42)ckeller2019-03-111-48/+47
* V8.7 (#36)ckeller2019-02-141-1/+0
* Merge from LFSC (#26)ckeller2019-01-281-33/+36
* Adding support for lemmas in the command veritQuentin Garchery2018-10-281-7/+9
* formattingQuentin Garchery2018-10-271-56/+56
* Command to bypass typechecking when generating a zchaff theoremChantal Keller2017-11-141-2/+6
* Corrected a bug with holes in proofsChantal Keller2016-10-071-1/+4
* Hopefully solved the problem with universes for the tacticChantal Keller2016-09-281-15/+40
* Uniform treatment of sat and smt tacticsChantal Keller2016-09-281-6/+2
* Improved performance with coq-8.5Chantal Keller2016-09-281-8/+19
* Print warnings when checking proofs with holesChantal Keller2016-04-301-5/+5
* Bring back the nice printing of automatically generated theoremsChantal Keller2016-04-301-3/+3
* Possibility to embed any Coq proof in certificates (not tested yet)Chantal Keller2016-04-291-11/+11
* Updating of the copyrightChantal Keller2016-04-271-2/+2
* Compatibility with native-coqChantal Keller2016-04-261-4/+4
* Tactic zchaff for 8.5Chantal Keller2016-04-261-5/+6
* Make the tactic available for 8.5Chantal Keller2016-04-261-1/+1
* Light port to Coq 8.5 under progressChantal Keller2016-03-181-3/+3
* Identify ML functions that are implemented differently in native-coq and in s...Chantal Keller2015-01-131-20/+5
* Identify ML functions that depend on native-coqChantal Keller2015-01-131-4/+4
* Initial import of SMTCoq v1.2Chantal Keller2015-01-121-0/+532