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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Corrected a bug with holes in proofs (for native-coq)	Chantal Keller	2016-10-07	1	-2/+2
\|
*	Hopefully solved the problem with universes for the tactic	Chantal Keller	2016-09-28	1	-0/+2
\|
*	Uniform treatment of sat and smt tactics	Chantal Keller	2016-09-28	2	-4/+3
\|
*	Improved performance with coq-8.5	Chantal Keller	2016-09-28	1	-1/+1
\|
*	More modularity on the format of traces depending on the version of coq	Chantal Keller	2016-09-23	4	-3/+72
\|
*	Now, Coq 8.5 is the default	Chantal Keller	2016-05-01	3	-8/+65
\|
*	Print warnings when checking proofs with holes	Chantal Keller	2016-04-30	1	-0/+5
\|
*	Bring back the nice printing of automatically generated theorems	Chantal Keller	2016-04-30	1	-1/+8
\|
*	Holes in proof:	Chantal Keller	2016-04-30	2	-2/+4
\| \| \| \| \| \| \|	- can now take learned clauses as argument - returns a whole clause (and not only a literal) - tested for the vernacular commands Warning: seems to slow down 8.5 version
*	Updating of the copyright	Chantal Keller	2016-04-27	1	-2/+2
\|
*	Both native-coq and Coq 8.5 are fully supported	Chantal Keller	2016-04-26	1	-1/+11
\|
*	Make the tactic available for 8.5	Chantal Keller	2016-04-26	1	-0/+2
\|
*	Light port to Coq 8.5 under progress	Chantal Keller	2016-03-18	3	-0/+603
\|
*	Removed old port to Coq 8.4	Chantal Keller	2016-03-02	3	-580/+0
\|
*	New targets [make vtest] and [make ztest] to perform unit tests for the ↵	Chantal Keller	2016-03-02	2	-1/+11
\| \| \| \|	various solvers separately
*	Corrected a bug introduced in native compilation	Chantal Keller	2015-02-12	1	-1/+2
\|
*	More on the support for standard Coq (not working yet)	Chantal Keller	2015-02-10	1	-0/+6
\|
*	Identify ML functions that are implemented differently in native-coq and in ↵	Chantal Keller	2015-01-13	1	-3/+25
\| \| \| \|	standard coq
*	Identify ML functions that depend on native-coq	Chantal Keller	2015-01-13	3	-0/+541