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

	Commit message (Expand)	Author	Age	Files	Lines
...
* \| \|	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
\|\\| \| \| \|
\| * \| \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq	Chantal Keller	2020-06-30	2	-12/+14
\| \|\ \ \ \ \| \| \| \|_\|/ \| \| \|/\| \|
\| * \| \| \|	Remove two axioms	Chantal Keller	2020-06-30	4	-19/+34
\| \| \|_\|/ \| \|/\| \|
* \| \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-06-30	2	-12/+14
\|\ \ \ \ \| \| \|/ / \| \|/\| \|
\| * \| \|	Cannot print stderr when calling CVC4	Chantal Keller	2020-06-30	1	-11/+13
\| * \| \|	Empty bit-vectors are not valid in SMT (fixes #76)	Chantal Keller	2020-06-30	1	-1/+1
\| \|/ /
* \| \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-06-29	1	-1/+5
\|\\| \|
\| * \|	Remove invalid axiom (see #71)	Chantal Keller	2020-06-29	1	-1/+5
* \| \|	Search and link package num correctly (#69)	Andres Erbsen	2020-06-29	2	-0/+6
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2020-05-15	2	-57/+75
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-05-15	2	-57/+75
\| \|\\|
\| \| *	Failure instead of exception when atom is not well-typed	Chantal Keller	2020-05-15	2	-5/+1
\| \| *	Typo	Chantal Keller	2020-05-15	1	-1/+0
\| \| *	Close #10	Chantal Keller	2020-05-15	1	-38/+55