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

	Commit message (Collapse)	Author	Age	Files	Lines
*	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.
*	Define substitution conformly to SMT-LIB	Chantal Keller	2020-07-20	5	-244/+47
\|
*	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
\|
*	Remove unused axiom	Chantal Keller	2020-06-30	1	-4/+0
\|
*	Remove axiom	Chantal Keller	2020-06-30	2	-5/+9
\|
*	Remove one axiom	Chantal Keller	2020-06-30	2	-55/+165
\|
*	Merge branch 'master' of github.com:smtcoq/smtcoq	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
\| \|
* \|	Remove two axioms	Chantal Keller	2020-06-30	4	-19/+34
\|/
*	Remove invalid axiom (see #71)	Chantal Keller	2020-06-29	1	-1/+5
\|
*	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
\|
*	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
\|
*	veriT does not distinguish between warnings and errors (#64)	Chantal Keller	2020-03-03	1	-0/+2
\|
*	Better error messages when veriT fails	Chantal Keller	2020-02-28	1	-3/+8
\|
*	Remove useless code	Chantal Keller	2020-02-28	1	-1/+1
\|
*	Revert "Search correctly for `num` library (#60)" (#61)	ckeller	2020-02-27	1	-4/+0
\| \| \|	This reverts commit dfbf0a5674ae1ab0dc68c15ae4b5df8cc439b741.
*	Search correctly for `num` library (#60)	Maxime Dénès	2020-02-25	1	-0/+4
\| \| \| \|	We fix the way SMTCoq searches for the num library, both when building and when generating .merlin.
*	Do not call Coqlib resolution at linking time (#59)	Maxime Dénès	2020-02-25	1	-2/+2
\| \| \| \| \| \|	This was triggering an exception in async mode (and probably with static linking too), where ML code is loaded before `.vo` files. Fixes #58
*	Documentation	Chantal Keller	2020-02-01	1	-0/+3
\|
*	Best practice on axiom	Chantal Keller	2020-01-28	1	-1/+2
\|
*	Best practice	Chantal Keller	2020-01-28	1	-0/+17
\|
*	Comments for conversion tactics	Chantal Keller	2020-01-21	1	-79/+92
\|
*	Changing notation for implb (closes #51)	Chantal Keller	2019-11-14	1	-6/+6
\|
*	Missing files	Chantal Keller	2019-09-25	2	-0/+60
\|
*	Made SmtCommands independent from VeritSyntax	Chantal Keller	2019-09-25	21	-298/+240
\| \| \| \|	Made lfsc/* mostly independent from VeritSyntax
*	Remove unused file	Chantal Keller	2019-09-20	1	-65/+0
\|
*	3rdparty	Chantal Keller	2019-07-15	11	-832/+106
\|
*	Separate unit tests into vernac and tactics	Chantal Keller	2019-04-12	3	-12/+7
\|
*	Properly check veriT exit code and warnings (#48)	ckeller	2019-04-12	5	-9/+17
\| \| \|	* Report veriT warnings
*	Error message to state that tactics are not supported with native-coq (#47)	ckeller	2019-04-12	8	-64/+148
\| \| \|	* Better error message for failing tactics with native-coq
*	Check again that veriT returns a zero exit code	Chantal Keller	2019-04-12	1	-1/+1
\|
*	Remove check of veriT non-zero exit code	Chantal Keller	2019-04-10	1	-1/+1
\|
*	V8.9 (#43)	ckeller	2019-03-15	17	-47/+2735
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* New syntax for implicit arguments * Towards 8.9: problems with Micromega plugin * Move to _CoqProject * Back to name Makefile * Switch to Makefile.local instead of -extra * The compilation issue is a Coq bug * Ok with 8.9 * INSTALL with 8.9 * Everything ok with 8.9
*	Support for native-coq	Chantal Keller	2019-03-12	2	-9/+14
\|
*	V8.8 (#42)	ckeller	2019-03-11	34	-1063/+1146
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	* Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Towards 8.8 * Organization structures * 8.8 ok with standard coq
*	No hard-coded paths to executables (fixes #37)	Chantal Keller	2019-03-05	4	-889/+6
\|
*	Compile with native-coq	Chantal Keller	2019-02-25	1	-3/+3
\|
*	Integer conversion now relies on the injection T2Z and its properties	Quentin Garchery	2019-02-25	1	-117/+76
\|
*	V8.7 (#36)	ckeller	2019-02-14	50	-1210/+1570
\| \| \|	Port SMTCoq to Coq-8.7
*	equalities on array and bv types (#34)	QGarchery	2019-02-12	2	-5/+5
\|
*	More on no_check	Chantal Keller	2019-02-08	1	-1/+1
\|
*	tactic notations (#31)	QGarchery	2019-02-08	1	-7/+7
\|