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

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12	Chantal Keller	2021-05-28	2	-9/+1
\|\
\| *	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-28	2	-7/+1
\| \|\
\| \| *	Get rid of most of our copy of micromega's source code (#94)	vblot	2021-05-28	2	-7/+1
* \| \|	Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12	Chantal Keller	2021-05-26	11	-11/+11
\|\\| \|
\| * \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-26	11	-11/+11
\| \|\\|
\| \| *	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-26	11	-11/+11
\| \| \|\
\| \| \| *	Update copyright	Chantal Keller	2021-05-26	11	-11/+11
* \| \| \|	Port ocaml part	Chantal Keller	2021-05-26	2	-5/+4
* \| \| \|	Port the Coq part	Chantal Keller	2021-05-26	1	-77/+69
\|/ / /
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-28	1	-1/+1
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-28	1	-1/+1
\| \|\\|
\| \| *	prop2bool_hyps insensitive to parenthesis	Chantal Keller	2021-04-28	1	-1/+1
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	1	-14/+17
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	1	-14/+17
\| \|\\|
\| \| *	CompDec are automatically discharged when generated by the OCaml tactic, when...	Chantal Keller	2021-04-26	1	-14/+17
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	1	-12/+115
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	1	-12/+115
\| \|\\|
\| \| *	Take hypotheses from the local context (#91)	ckeller	2021-04-26	1	-12/+115
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-21	3	-30/+15
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-21	3	-30/+15
\| \|\\|
\| \| *	Convert hypotheses from Prop to bool (#89)	ckeller	2021-04-21	3	-30/+15
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-02-23	1	-6/+6
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-02-23	1	-6/+6
\| \|\\|
\| \| *	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	1	-6/+6
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-06-29	1	-1/+5
\| \|\\|
* \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-06-29	1	-1/+5
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Remove invalid axiom (see #71)	Chantal Keller	2020-06-29	1	-1/+5
* \| \|	Search and link package num correctly (#69)	Andres Erbsen	2020-06-29	1	-0/+4
* \| \|	Compiles with Coq-8.11	Chantal Keller	2020-04-01	2	-30/+19
\| \|/ \|/\|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-03-31	2	-9/+36
\|\\|
\| *	Test asynchronous and make the selected lemmas persistant (#66)	ckeller	2020-03-26	2	-5/+28
\| *	make test does not need cleaning anymore	Chantal Keller	2020-03-25	1	-4/+4
\| *	Revert "Search correctly for `num` library (#60)" (#61)	ckeller	2020-02-27	1	-4/+0
\| *	Search correctly for `num` library (#60)	Maxime Dénès	2020-02-25	1	-0/+4
* \|	Compiles with Coq-8.10	Chantal Keller	2020-03-31	2	-0/+2
* \|	Port to coq-8.10 under progress	Chantal Keller	2020-03-31	7	-2670/+22
* \|	Hints in databases	Chantal Keller	2020-01-28	2	-0/+3
* \|	Towards coqpp	Chantal Keller	2020-01-16	1	-35/+35
* \|	ml4 -> mlg	Chantal Keller	2020-01-16	2	-1/+1
\|/
*	Made SmtCommands independent from VeritSyntax	Chantal Keller	2019-09-25	2	-0/+3
*	3rdparty	Chantal Keller	2019-07-15	2	-9/+11
*	Separate unit tests into vernac and tactics	Chantal Keller	2019-04-12	1	-1/+1
*	Properly check veriT exit code and warnings (#48)	ckeller	2019-04-12	2	-0/+2
*	Error message to state that tactics are not supported with native-coq (#47)	ckeller	2019-04-12	2	-0/+66
*	V8.9 (#43)	ckeller	2019-03-15	8	-32/+2703
*	V8.8 (#42)	ckeller	2019-03-11	5	-208/+264
*	No hard-coded paths to executables (fixes #37)	Chantal Keller	2019-03-05	3	-887/+2
*	V8.7 (#36)	ckeller	2019-02-14	10	-644/+997
*	Cleanup	Chantal Keller	2019-01-29	2	-7/+1
*	Merge from LFSC (#26)	ckeller	2019-01-28	13	-82/+227