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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Update copyright	Chantal Keller	2021-05-26	1	-1/+1
\|
*	Take hypotheses from the local context (#91)	ckeller	2021-04-26	1	-5/+5
\| \| \| \| \|	* 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)
*	Convert hypotheses from Prop to bool (#89)	ckeller	2021-04-21	1	-2/+2
\| \| \| \| \| \| \|	* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed. * Some current limitations are detailed in src/PropToBool.v. * Partially enhances #30 .
*	Example of groups in unit tests	Chantal Keller	2021-02-23	1	-18/+37
\|
*	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	1	-1/+89
\| \| \| \| \|	Equality is now treated from uninterpreted sorts, which makes them usable with tactics! Closes #17 Closes #78
*	Testing BV subtraction	Chantal Keller	2020-07-20	1	-0/+16
\|
*	Test asynchronous and make the selected lemmas persistant (#66)	ckeller	2020-03-26	1	-72/+83
\| \| \| \| \| \| \|	* Add a test target for asynchronous proof checking (does not fully reflect the coqide behavior though) * Make the selected lemmas persistant Co-authored-by: Chantal Keller <Chantal.Keller@lri.fr>
*	Add the full example of the webpage in the unit tests	Chantal Keller	2020-01-16	1	-0/+30
\|
*	Separate unit tests into vernac and tactics	Chantal Keller	2019-04-12	1	-0/+705