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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Bring back the nice printing of automatically generated theorems	Chantal Keller	2016-04-30	1	-1/+0
\|
*	Holes in proof:	Chantal Keller	2016-04-30	2	-1/+38
\| \| \| \| \| \| \|	- 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
*	Possibility to embed any Coq proof in certificates (not tested yet)	Chantal Keller	2016-04-29	1	-30/+30
\|
*	Both native-coq and Coq 8.5 are fully supported	Chantal Keller	2016-04-26	1	-18/+14
\|
*	English comments	Chantal Keller	2016-04-26	2	-5/+5
\|
*	Compatibility with native-coq	Chantal Keller	2016-04-26	1	-8/+8
\|
*	- Solved the Coq 8.5 problem relating to declaring section variables	Chantal Keller	2016-04-26	1	-3/+3
\| \| \| \|	- Correct equality check of atoms and formulas for processing congruence closure
*	The simplest test for SMT	Chantal Keller	2016-04-24	2	-0/+17
\|
*	Port to 8.5: how to deal with universe constraints	Chantal Keller	2016-03-23	1	-5/+0
\|
*	Light port to Coq 8.5 under progress	Chantal Keller	2016-03-18	1	-0/+5
\|
*	New targets [make vtest] and [make ztest] to perform unit tests for the ↵	Chantal Keller	2016-03-02	3	-423/+427
\| \| \| \|	various solvers separately
*	The current version of SMTCoq does not support SMTLIB "let" anymore	Chantal Keller	2016-03-02	1	-0/+6
\|
*	All tests (but large benchmarks) succeed	Chantal Keller	2015-02-11	1	-7/+6
\|
*	Unit test for double negation	Chantal Keller	2015-01-12	1	-0/+4
\|
*	"let" testsv1.2	Chantal Keller	2015-01-12	1	-21/+21
\|
*	Initial import of SMTCoq v1.2	Chantal Keller	2015-01-12	43	-0/+23483