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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Allow premices of the transitivity rule to be reflexivity lemmas	Chantal Keller	2016-11-02	1	-8/+15
\|
*	Corrected a bug with holes in proofs	Chantal Keller	2016-10-07	1	-2/+2
\|
*	Correct parsing of <-> for veriT	Chantal Keller	2016-05-02	1	-0/+2
\|
*	Holes in proof:	Chantal Keller	2016-04-30	4	-4/+8
\| \| \| \| \| \| \|	- 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	5	-10/+13
\|
*	Both native-coq and Coq 8.5 are fully supported	Chantal Keller	2016-04-26	2	-3/+3
\|
*	- Solved the Coq 8.5 problem relating to declaring section variables	Chantal Keller	2016-04-26	1	-8/+8
\| \| \| \|	- Correct equality check of atoms and formulas for processing congruence closure
*	Code refactoring	Chantal Keller	2016-03-02	1	-354/+10
\|
*	Separate verit input (smtlib2) from output	Chantal Keller	2016-03-02	5	-831/+0
\|
*	Identify ML functions that are implemented differently in native-coq and in ↵	Chantal Keller	2015-01-13	1	-49/+9
\| \| \| \|	standard coq
*	Identify ML functions that depend on native-coq	Chantal Keller	2015-01-13	1	-6/+6
\|
*	Initial import of SMTCoq v1.2	Chantal Keller	2015-01-12	10	-0/+2124