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

	Commit message (Expand)	Author	Age	Files	Lines
*	V8.7 (#36)	ckeller	2019-02-14	2	-47/+42
*	equalities on array and bv types (#34)	QGarchery	2019-02-12	1	-1/+1
*	Fix passing the goal strongly hashed (in ra' rf') instead of normal goal (has...	QGarchery	2019-02-07	2	-22/+22
*	Merge from LFSC (#26)	ckeller	2019-01-28	6	-275/+532
*	verit also works when it doesn't use the conclusion (#24)	QGarchery	2018-12-03	1	-28/+3
*	forall declaration can now begin with a negation (#23)	QGarchery	2018-11-30	2	-2/+2
*	Adding support for lemmas in the command verit	Quentin Garchery	2018-10-28	6	-114/+378
*	New files SmtBtype.ml(i) for module formerly in SmtAtom	Quentin Garchery	2018-10-28	4	-11/+11
*	formatting	Quentin Garchery	2018-10-27	3	-192/+194
*	now compiles with standard coq (including 8.6.1 from opam)	Valentin Blot	2018-07-20	1	-1/+1
*	- auto-generated mli files for future documentation	Valentin Blot	2017-11-24	1	-0/+31
*	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
*	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
*	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 s...	Chantal Keller	2015-01-13	1	-49/+9
*	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