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

	Commit message (Collapse)	Author	Age	Files	Lines
*	prop2bool_hyps insensitive to parenthesis	Chantal Keller	2021-04-28	1	-1/+1
\|
*	CompDec are automatically discharged when generated by the OCaml tactic, ↵	Chantal Keller	2021-04-26	1	-14/+17
\| \| \| \|	when possible
*	Take hypotheses from the local context (#91)	ckeller	2021-04-26	1	-12/+115
\| \| \| \| \|	* 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	-27/+13
\| \| \| \| \| \| \|	* 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 .
*	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	1	-6/+6
\| \| \| \| \|	Equality is now treated from uninterpreted sorts, which makes them usable with tactics! Closes #17 Closes #78
*	Error message to state that tactics are not supported with native-coq (#47)	ckeller	2019-04-12	1	-0/+65
	* Better error message for failing tactics with native-coq