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.11	Chantal Keller	2021-04-28	4	-4/+32
\|\
\| *	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-28	4	-4/+32
\| \|\
\| \| *	Solve a bug when reifying under a binder	Chantal Keller	2021-04-28	4	-4/+32
* \| \|	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	3	-4/+64
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	3	-4/+64
\| \|\\|
\| \| *	Equality between Booleans should be changed for hypotheses	Chantal Keller	2021-04-26	3	-4/+64
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	2	-18/+30
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	2	-18/+30
\| \|\\|
\| \| *	CompDec are automatically discharged when generated by the OCaml tactic, when...	Chantal Keller	2021-04-26	2	-18/+30
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	6	-85/+241
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-26	6	-85/+241
\| \|\\|
\| \| *	Take hypotheses from the local context (#91)	ckeller	2021-04-26	6	-85/+241
* \| \|	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	15	-161/+484
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-21	15	-161/+484
\| \|\\|
\| \| *	Convert hypotheses from Prop to bool (#89)	ckeller	2021-04-21	15	-161/+484
* \| \|	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	1	-1/+1
\|\\| \|
\| * \|	Batch parallelism	Chantal Keller	2021-02-23	1	-1/+1
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-02-23	2	-28/+42
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-02-23	2	-28/+42
\| \|\\|
\| \| *	Example of groups in unit tests	Chantal Keller	2021-02-23	1	-18/+37
\| \| *	The examples on lists uses the true list type	Chantal Keller	2021-02-23	1	-10/+5
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-02-23	20	-290/+740
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-02-23	20	-290/+740
\| \|\\|
\| \| *	Link equality on uninterpreted sorts with SMT equality (#86)	ckeller	2021-02-23	18	-290/+683
\| \| *	Add ci manifest to compile from the sources	grianneau	2021-01-27	2	-0/+57
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-01-13	1	-1/+1
\|\\| \|
\| * \|	Version of OCaml	Chantal Keller	2021-01-13	1	-2/+2
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-01-13	3	-9/+117
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-01-13	3	-9/+117
\| \|\\|
\| \| *	Reify polymorphic terms	ckeller	2021-01-05	3	-9/+117
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-01-05	2	-7/+7
\| \|\\|