aboutsummaryrefslogtreecommitdiffstats
path: root/src/zchaff
Commit message (Expand)AuthorAgeFilesLines
* Extraction for Coq 8.13 (#109)ckeller2022-07-301-0/+8
* Merge remote-tracking branch 'origin/master' into coq-8.10Chantal Keller2022-02-178-8/+8
|\
| * Update copyrightChantal Keller2022-02-168-8/+8
* | Use the Register mechanism (#104)ckeller2022-02-151-24/+18
* | getting rid of native-coq (#95)vblot2021-05-282-63/+63
* | Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10Chantal Keller2021-05-268-8/+8
|\|
| * Update copyrightChantal Keller2021-05-268-8/+8
* | Port to coq-8.10 under progressChantal Keller2020-03-311-1/+1
|/
* V8.8 (#42)ckeller2019-03-112-51/+50
* V8.7 (#36)ckeller2019-02-143-3/+2
* Merge from LFSC (#26)ckeller2019-01-288-137/+94
* compatibility with safe-strings (ocaml >= 4.06.0)Valentin Blot2018-11-062-18/+18
* Adding support for lemmas in the command veritQuentin Garchery2018-10-283-10/+12
* formattingQuentin Garchery2018-10-271-56/+56
* now compiles with standard coq (including 8.6.1 from opam)Valentin Blot2018-07-201-2/+2
* - auto-generated mli files for future documentationValentin Blot2017-11-244-0/+170
* 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-274-8/+12
* 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-124-0/+928
generated by cgit (git 2.34.1) at 2024-05-18 22:37:59 +0000