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

	Commit message (Expand)	Author	Age	Files	Lines
*	Another silent change of veriT...	Chantal Keller	2021-05-06	1	-0/+22
*	Example for #92	Chantal Keller	2021-05-06	1	-0/+12
*	CompDec on interpreted type	Chantal Keller	2021-05-05	1	-0/+35
*	Reify applied polymorphic terms with compdec	Chantal Keller	2021-05-05	1	-0/+31
*	Solve a bug when reifying under a binder	Chantal Keller	2021-04-28	1	-0/+14
*	Equality between Booleans should be changed for hypotheses	Chantal Keller	2021-04-26	1	-0/+11
*	CompDec are automatically discharged when generated by the OCaml tactic, when...	Chantal Keller	2021-04-26	1	-4/+13
*	Take hypotheses from the local context (#91)	ckeller	2021-04-26	1	-52/+46
*	Convert hypotheses from Prop to bool (#89)	ckeller	2021-04-21	1	-38/+171
*	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
*	Reify polymorphic terms	ckeller	2021-01-05	1	-0/+10
*	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
*	Separate unit tests into vernac and tactics	Chantal Keller	2019-04-12	1	-0/+966