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

	Commit message (Collapse)	Author	Age	Files	Lines
...
\| *	Equality between Booleans should be changed for hypotheses	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	1	-14/+17
\|\\|
\| *	CompDec are automatically discharged when generated by the OCaml tactic, ↵	Chantal Keller	2021-04-26	1	-14/+17
\| \| \| \| \| \| \| \|	when possible
* \|	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
\| \| \| \| \| \| \| \| \| \|	* 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	12	-113/+304
\|\\|
\| *	Convert hypotheses from Prop to bool (#89)	ckeller	2021-04-21	12	-113/+304
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	* 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
\| \|
* \|	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
\| \| \| \| \| \| \| \| \| \|	Equality is now treated from uninterpreted sorts, which makes them usable with tactics! Closes #17 Closes #78
* \|	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
\| \| \| \| \| \|	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	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.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 '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
\| \|
* \|	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	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.10	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.10	Chantal Keller	2020-06-29	1	-1/+5
\|\\|
\| *	Remove invalid axiom (see #71)	Chantal Keller	2020-06-29	1	-1/+5
\| \|
* \|	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
\| \|
\| *	Solve bug in SMT print	Chantal Keller	2020-05-15	1	-17/+23
\| \|
\| *	More precise call to Micromega	Chantal Keller	2020-05-15	1	-1/+1
\| \|
* \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2020-03-31	5	-14/+52
\|\\|
\| *	Test asynchronous and make the selected lemmas persistant (#66)	ckeller	2020-03-26	2	-5/+28
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	* Add a test target for asynchronous proof checking (does not fully reflect the coqide behavior though) * Make the selected lemmas persistant Co-authored-by: Chantal Keller <Chantal.Keller@lri.fr>
\| *	make test does not need cleaning anymore	Chantal Keller	2020-03-25	1	-4/+4
\| \|