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-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
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-01-13	2	-9/+107
\| \|\\|
\| \| *	Reify polymorphic terms	ckeller	2021-01-05	2	-9/+107
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-07-20	5	-244/+47
\| \|\\|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-07-06	4	-23/+130
\| \|\ \
\| * \ \	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-06-30	3	-9/+9
\| \|\ \ \
\| * \ \ \	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-06-30	2	-55/+165
\| \|\ \ \ \
\| * \ \ \ \	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-06-30	4	-19/+34
\| \|\ \ \ \ \
\| * \ \ \ \ \	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-06-30	2	-12/+14
\| \|\ \ \ \ \ \
\| * \ \ \ \ \ \	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-06-29	1	-1/+5
\| \|\ \ \ \ \ \ \
* \| \ \ \ \ \ \ \	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-07-20	5	-244/+47
\|\ \ \ \ \ \ \ \ \ \| \| \|_\|_\|_\|_\|_\|_\|/ \| \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Define substitution conformly to SMT-LIB	Chantal Keller	2020-07-20	5	-244/+47
\| \| \|_\|_\|_\|_\|_\|/ \| \|/\| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-07-06	4	-23/+130
\|\\| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	Clarify axiom usage (closes #71)	Chantal Keller	2020-07-06	1	-2/+6
\| * \| \| \| \| \| \|	Use officiel library for proof irrelevance	Chantal Keller	2020-07-01	2	-5/+4
\| * \| \| \| \| \| \|	Got rid of classical epsilon	Chantal Keller	2020-06-30	1	-16/+120
\| \| \|_\|_\|_\|_\|/ \| \|/\| \| \| \| \|
* \| \| \| \| \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-06-30	3	-9/+9
\|\\| \| \| \| \| \|
\| * \| \| \| \| \|	Remove unused axiom	Chantal Keller	2020-06-30	1	-4/+0
\| * \| \| \| \| \|	Remove axiom	Chantal Keller	2020-06-30	2	-5/+9
\| \| \|_\|_\|_\|/ \| \|/\| \| \| \|
* \| \| \| \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-06-30	2	-55/+165
\|\\| \| \| \| \|
\| * \| \| \| \|	Remove one axiom	Chantal Keller	2020-06-30	2	-55/+165
\| \| \|_\|_\|/ \| \|/\| \| \|
* \| \| \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-06-30	4	-19/+34
\|\\| \| \| \|