smtcoq - Fork of https://github.com/smtcoq/smtcoq.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Command to bypass typechecking when generating a zchaff theorem	Chantal Keller	2017-11-14	1	-2/+6
\|
*	Corrected a bug with holes in proofs	Chantal Keller	2016-10-07	1	-1/+4
\|
*	Hopefully solved the problem with universes for the tactic	Chantal Keller	2016-09-28	1	-15/+40
\|
*	Uniform treatment of sat and smt tactics	Chantal Keller	2016-09-28	1	-6/+2
\|
*	Improved performance with coq-8.5	Chantal Keller	2016-09-28	1	-8/+19
\|
*	Print warnings when checking proofs with holes	Chantal Keller	2016-04-30	1	-5/+5
\|
*	Bring back the nice printing of automatically generated theorems	Chantal Keller	2016-04-30	1	-3/+3
\|
*	Possibility to embed any Coq proof in certificates (not tested yet)	Chantal Keller	2016-04-29	1	-11/+11
\|
*	Updating of the copyright	Chantal Keller	2016-04-27	4	-8/+12
\|
*	Compatibility with native-coq	Chantal Keller	2016-04-26	1	-4/+4
\|
*	Tactic zchaff for 8.5	Chantal Keller	2016-04-26	1	-5/+6
\|
*	Make the tactic available for 8.5	Chantal Keller	2016-04-26	1	-1/+1
\|
*	Light port to Coq 8.5 under progress	Chantal Keller	2016-03-18	1	-3/+3
\|
*	Identify ML functions that are implemented differently in native-coq and in ↵	Chantal Keller	2015-01-13	1	-20/+5
\| \| \| \|	standard coq
*	Identify ML functions that depend on native-coq	Chantal Keller	2015-01-13	1	-4/+4
\|
*	Initial import of SMTCoq v1.2	Chantal Keller	2015-01-12	4	-0/+928