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

	Commit message (Collapse)	Author	Age	Files	Lines
*	The examples on lists uses the true list type	Chantal Keller	2021-02-23	1	-10/+5
\|
*	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	1	-26/+129
\| \| \| \| \|	Equality is now treated from uninterpreted sorts, which makes them usable with tactics! Closes #17 Closes #78
*	Reify polymorphic terms	ckeller	2021-01-05	1	-0/+10
\| \| \|	A polymorphic term is now reified as a whole of the term applied to one or many types. The same polymorphic term applied to different types is reified as different monomorphic terms.
*	Close #10	Chantal Keller	2020-05-15	1	-0/+18
\|
*	Test asynchronous and make the selected lemmas persistant (#66)	ckeller	2020-03-26	1	-106/+118
\| \| \| \| \| \| \|	* 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>
*	Separate unit tests into vernac and tactics	Chantal Keller	2019-04-12	1	-0/+966