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

	Commit message (Collapse)	Author	Age	Files	Lines
...
\| *	CompDec are automatically discharged when generated by the OCaml tactic, ↵	Chantal Keller	2021-04-26	2	-18/+30
\| \| \| \| \| \| \| \|	when possible
* \|	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
\| \| \| \| \| \| \| \| \| \|	* The tactics sets veritXXX and smtXXX now automatically take hypotheses from the local context * `prop2bool_hyps` also apply to hypotheses not in the local context * Second strategy for vauto (still incomplete)
* \|	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 ↵	Chantal Keller	2021-04-21	1	-15/+15
\| \| \| \| \| \| \| \|	hypotheses
* \|	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
\| \|
* \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	* This PR converts hypotheses given to the tactics verit, verit_no_check, smt and smt_no_check from Prop to bool when needed. * Some current limitations are detailed in src/PropToBool.v. * Partially enhances #30 .
* \|	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
\| \|
* \|	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
\| \|
* \|	Batch parallelism	Chantal Keller	2021-02-23	1	-1/+1
\| \|
* \|	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 '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
\| \| \| \| \| \| \| \| \| \|	Equality is now treated from uninterpreted sorts, which makes them usable with tactics! Closes #17 Closes #78
\| *	Add ci manifest to compile from the sources	grianneau	2021-01-27	2	-0/+57
\| \| \| \| \| \| \| \|	* compiling SMTCoq from sources from branch 8.11 * manifest using debian/stable to make it work with OCaml 8.09.1
* \|	Version of OCaml	Chantal Keller	2021-01-13	1	-2/+2
\| \|
* \|	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
\| \| \| \| \| \|	A polymorphic term is now reified as a whole of the term applied to one or many types. The same polymorphic term applied to different types is reified as different monomorphic terms.
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-01-05	2	-7/+7
\|\\|
\| *	Change imports from `SMTCoq` to `SMTCoq.SMTCoq` (#83)	XZ-X	2021-01-05	2	-7/+7
\| \| \| \| \| \| \| \| \| \|	* Update USE.md and `README.md` Change the imports in `USE.md` and `README.md` from `SMTCoq` to `SMTCoq.SMTCoq`
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-08-28	1	-0/+75
\|\\|
\| *	Full docker script	Chantal Keller	2020-08-28	1	-2/+15
\| \|
\| *	Creating a docker container	Chantal Keller	2020-08-28	1	-0/+62
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-07-20	1	-0/+16
\|\\|
\| *	Testing BV subtraction	Chantal Keller	2020-07-20	1	-0/+16
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-07-20	5	-244/+47
\|\\|
\| *	Define substitution conformly to SMT-LIB	Chantal Keller	2020-07-20	5	-244/+47
\| \|
* \|	Update installation instructions	Chantal Keller	2020-07-20	1	-5/+5
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-07-20	1	-4/+4
\|\\|
\| *	Installation instructions for 8.9.1	Chantal Keller	2020-07-20	1	-4/+4
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-07-20	1	-50/+63
\|\\|
\| *	Update installation instructions	Chantal Keller	2020-07-20	1	-50/+63
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	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 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-07-06	43	-3223/+896
\|\ \
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	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.10	Chantal Keller	2020-06-30	2	-55/+165
\| \|\\|
\| \| *	Remove one axiom	Chantal Keller	2020-06-30	2	-55/+165
\| \| \|