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

	Commit message (Collapse)	Author	Age	Files	Lines
...
*	Compiles with Coq-8.6	Chantal Keller	2017-10-03	7	-97/+245
\|
*	Some proofs for the Int63 glue	Chantal Keller	2016-10-14	1	-8/+104
\|
*	Some proofs for the Int63 glue	Chantal Keller	2016-10-10	6	-125/+192
\|
*	Corrected a bug with holes in proofs (for native-coq)	Chantal Keller	2016-10-07	1	-2/+2
\|
*	Corrected a bug with holes in proofs	Chantal Keller	2016-10-07	1	-2/+2
\|
*	(Hopefully) repared the universes problems	Chantal Keller	2016-10-07	1	-1/+4
\|
*	Hopefully solved the problem with universes for the tactic	Chantal Keller	2016-09-28	2	-0/+8
\|
*	Uniform treatment of sat and smt tactics	Chantal Keller	2016-09-28	4	-8/+6
\|
*	Improved performance with coq-8.5	Chantal Keller	2016-09-28	2	-3/+3
\|
*	Use the most efficient operations of Int31	Chantal Keller	2016-09-28	2	-47/+34
\|
*	Use the Int31 library with coq-8.5	Chantal Keller	2016-09-28	6	-3141/+0
\|
*	More straightforward definitions in Int63Native_standard	Chantal Keller	2016-09-26	1	-32/+32
\|
*	More modularity on the format of traces depending on the version of coq	Chantal Keller	2016-09-23	8	-9/+132
\|
*	Now, Coq 8.5 is the default	Chantal Keller	2016-05-01	6	-18/+134
\|
*	Print warnings when checking proofs with holes	Chantal Keller	2016-04-30	2	-0/+10
\|
*	Bring back the nice printing of automatically generated theorems	Chantal Keller	2016-04-30	2	-2/+23
\|
*	Holes in proof:	Chantal Keller	2016-04-30	4	-9/+61
\| \| \| \| \| \| \|	- can now take learned clauses as argument - returns a whole clause (and not only a literal) - tested for the vernacular commands Warning: seems to slow down 8.5 version
*	Updating of the copyright	Chantal Keller	2016-04-27	11	-54/+91
\|
*	Both native-coq and Coq 8.5 are fully supported	Chantal Keller	2016-04-26	2	-2/+24
\|
*	Make the tactic available for 8.5	Chantal Keller	2016-04-26	2	-0/+4
\|
*	- Solved the Coq 8.5 problem relating to declaring section variables	Chantal Keller	2016-04-26	1	-2/+2
\| \| \| \|	- Correct equality check of atoms and formulas for processing congruence closure
*	Port to 8.5: how to deal with universe constraints	Chantal Keller	2016-03-23	1	-3/+7
\|
*	Solved a dependency problem for the compilation with Coq 8.5	Chantal Keller	2016-03-21	2	-7/+4
\|
*	Light port to Coq 8.5 under progress	Chantal Keller	2016-03-18	15	-0/+8162
\|
*	Removed old port to Coq 8.4	Chantal Keller	2016-03-02	15	-7966/+0
\|
*	New targets [make vtest] and [make ztest] to perform unit tests for the ↵	Chantal Keller	2016-03-02	2	-1/+11
\| \| \| \|	various solvers separately
*	Corrected a bug introduced in native compilation	Chantal Keller	2015-02-12	1	-1/+2
\|
*	Implemented cast on int31 directly	Chantal Keller	2015-02-11	3	-61/+114
\|
*	COrrect implementation of foldi_cont and foldi_down_cont	Chantal Keller	2015-02-11	1	-6/+6
\|
*	More efficient initialization of an array	Chantal Keller	2015-02-11	1	-7/+3
\|
*	Corrected a bug in the initialization of arrays for the standard version ↵	Chantal Keller	2015-02-11	1	-2/+7
\| \| \| \|	(the last element is the default)
*	More on the support for standard Coq (not working yet)	Chantal Keller	2015-02-10	8	-61/+112
\|
*	Frontend for the standard version of Coq (still bad computational behavior)	Chantal Keller	2015-02-10	11	-325/+3548
\|
*	Start porting to the standard version of Coq (not finished yet)	Chantal Keller	2015-01-13	9	-0/+4064
\|
*	Identify ML functions that are implemented differently in native-coq and in ↵	Chantal Keller	2015-01-13	1	-3/+25
\| \| \| \|	standard coq
*	Identify ML functions that depend on native-coq	Chantal Keller	2015-01-13	3	-0/+541