aboutsummaryrefslogtreecommitdiffstats
path: root/src/zchaff/zchaff.ml
Commit message (Expand)AuthorAgeFilesLines
* Update copyrightChantal Keller2021-05-261-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
generated by cgit (git 2.34.1) at 2024-06-26 15:51:00 +0000