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

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge remote-tracking branch 'origin/master' into coq-8.10	Chantal Keller	2022-02-17	1	-1/+1
\|\
\| *	Update copyright	Chantal Keller	2022-02-16	1	-1/+1
* \|	getting rid of native-coq (#95)	vblot	2021-05-28	1	-1/+1
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-26	1	-1/+1
\|\\|
\| *	Update copyright	Chantal Keller	2021-05-26	1	-1/+1
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-02-23	1	-5/+5
\|\\|
\| *	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	1	-5/+5
* \|	Compiles with Coq-8.10	Chantal Keller	2020-03-31	1	-2/+2
\|/
*	Made SmtCommands independent from VeritSyntax	Chantal Keller	2019-09-25	1	-42/+9
*	V8.7 (#36)	ckeller	2019-02-14	1	-14/+14
*	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	1	-2/+2
*	Merge from LFSC (#26)	ckeller	2019-01-28	1	-149/+278
*	forall declaration can now begin with a negation (#23)	QGarchery	2018-11-30	1	-1/+1
*	Adding support for lemmas in the command verit	Quentin Garchery	2018-10-28	1	-12/+141
*	New files SmtBtype.ml(i) for module formerly in SmtAtom	Quentin Garchery	2018-10-28	1	-1/+1
*	formatting	Quentin Garchery	2018-10-27	1	-182/+184
*	Allow premices of the transitivity rule to be reflexivity lemmas	Chantal Keller	2016-11-02	1	-8/+15
*	Holes in proof:	Chantal Keller	2016-04-30	1	-1/+3
*	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/+1
*	- Solved the Coq 8.5 problem relating to declaring section variables	Chantal Keller	2016-04-26	1	-8/+8
*	Initial import of SMTCoq v1.2	Chantal Keller	2015-01-12	1	-0/+355