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

	Commit message (Collapse)	Author	Age	Files	Lines
*	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-05-25	1	-8/+1
\|\\|
\| *	CompDec clean-up (#93)	ckeller	2021-05-25	1	-8/+1
\| \| \| \| \| \|	Clean-up the definition of CompDec, leaving the required minimum (in particular for functional arrays)
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-06	1	-0/+11
\|\\|
\| *	Another silent change of veriT...	Chantal Keller	2021-05-06	1	-0/+11
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	1	-1/+42
\|\\|
\| *	Equality between Booleans should be changed for hypotheses	Chantal Keller	2021-04-26	1	-1/+42
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	1	-12/+62
\|\\|
\| *	Take hypotheses from the local context (#91)	ckeller	2021-04-26	1	-12/+62
\| \| \| \| \| \| \| \| \| \|	* The tactics sets veritXXX and smtXXX now automatically take hypotheses from the local context * `prop2bool_hyps` also apply to hypotheses not in the local context * Second strategy for vauto (still incomplete)
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-02-23	1	-10/+54
\|\\|
\| *	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	1	-10/+54
\| \| \| \| \| \| \| \| \| \|	Equality is now treated from uninterpreted sorts, which makes them usable with tactics! Closes #17 Closes #78
* \|	Compiles with Coq-8.10	Chantal Keller	2020-03-31	1	-1/+1
\| \|
* \|	Hint DB for QInst	Chantal Keller	2020-01-28	1	-1/+1
\|/
*	Error message to state that tactics are not supported with native-coq (#47)	ckeller	2019-04-12	1	-0/+80
	* Better error message for failing tactics with native-coq