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

	Commit message (Expand)	Author	Age	Files	Lines
*	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11pxtp21	Chantal Keller	2021-05-06	1	-0/+11
\|\
\| *	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 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-06	1	-11/+1
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-06	1	-11/+1
\| \|\\|
\| \| *	Less instances needed for auto	Chantal Keller	2021-05-06	1	-11/+1
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-05	2	-2/+1
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-05	2	-2/+1
\| \|\\|
\| \| *	CompDec on interpreted type	Chantal Keller	2021-05-05	2	-2/+1
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-05	3	-3/+32
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-05	3	-3/+32
\| \|\\|
\| \| *	Reify applied polymorphic terms with compdec	Chantal Keller	2021-05-05	3	-3/+32
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-28	3	-4/+18
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-28	3	-4/+18
\| \|\\|
\| \| *	Solve a bug when reifying under a binder	Chantal Keller	2021-04-28	3	-4/+18
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-28	2	-3/+3
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-28	2	-3/+3
\| \|\\|
\| \| *	prop2bool_hyps insensitive to parenthesis	Chantal Keller	2021-04-28	2	-3/+3
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	2	-4/+53
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	2	-4/+53
\| \|\\|
\| \| *	Equality between Booleans should be changed for hypotheses	Chantal Keller	2021-04-26	2	-4/+53
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	1	-14/+17
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	1	-14/+17
\| \|\\|
\| \| *	CompDec are automatically discharged when generated by the OCaml tactic, when...	Chantal Keller	2021-04-26	1	-14/+17
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	4	-28/+190
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	4	-28/+190
\| \|\\|
\| \| *	Take hypotheses from the local context (#91)	ckeller	2021-04-26	4	-28/+190
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-21	1	-15/+15
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-21	1	-15/+15
\| \|\\|
\| \| *	Solve a bound variable capture problem in the reification of quantified hypot...	Chantal Keller	2021-04-21	1	-15/+15
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-21	5	-16/+57
\|\\| \|
\| * \|	Port to 8.10	Chantal Keller	2021-04-21	1	-1/+1
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-21	5	-16/+57
\| \|\\|
\| \| *	Warning (instead of error) for unsupported lemmas (#90)	ckeller	2021-04-21	5	-16/+57
* \| \|	Port to 8.11	Chantal Keller	2021-04-21	1	-2/+2
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-21	12	-113/+304
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-21	12	-113/+304
\| \|\\|
\| \| *	Convert hypotheses from Prop to bool (#89)	ckeller	2021-04-21	12	-113/+304
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-01	1	-1/+99
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-01	1	-1/+99
\| \|\\|
\| \| *	CompDec on lists	Chantal Keller	2021-04-01	1	-1/+99
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-01	2	-3/+4
\|\\| \|
\| * \|	Un-backport #87	Chantal Keller	2021-04-01	1	-1/+1
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-01	2	-3/+4
\| \|\\|
\| \| *	Backport #87 to Coq-8.9 (closes #87)	Chantal Keller	2021-04-01	1	-1/+1
\| \| *	use is_true from standard library	lduboisd	2021-04-01	2	-3/+4
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-02-23	15	-228/+416
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-02-23	15	-228/+416
\| \|\\|
\| \| *	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	15	-228/+416
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-01-13	2	-9/+107
\|\\| \|