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

	Commit message (Collapse)	Author	Age	Files	Lines
...
\| * \| \| \|	Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12	Chantal Keller	2021-05-28	2	-866/+4
\| \|\\| \| \|
\| \| * \| \|	Configure is back (due to #69)	Chantal Keller	2021-05-28	2	-828/+4
\| \| \| \| \|
* \| \| \| \|	Merge branch 'coq-8.12' of github.com:smtcoq/smtcoq into coq-8.13	Chantal Keller	2021-05-28	56	-2108/+1672
\|\\| \| \| \|
\| * \| \| \|	Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12	Chantal Keller	2021-05-28	56	-2108/+1672
\| \|\\| \| \|
\| \| * \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-28	56	-2107/+1634
\| \| \|\\| \|
\| \| \| * \|	Add Makefile	Chantal Keller	2021-05-28	1	-0/+801
\| \| \| \| \|
\| \| \| * \|	getting rid of native-coq (#95)	vblot	2021-05-28	55	-2105/+804
\| \| \| \| \|
* \| \| \| \|	Merge branch 'coq-8.12' of github.com:smtcoq/smtcoq into coq-8.13	Chantal Keller	2021-05-28	5	-202/+10
\|\\| \| \| \|
\| * \| \| \|	Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12	Chantal Keller	2021-05-28	5	-202/+10
\| \|\\| \| \|
\| \| * \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-28	5	-201/+10
\| \| \|\\| \|
\| \| \| * \|	Get rid of most of our copy of micromega's source code (#94)	vblot	2021-05-28	5	-179/+10
\| \| \| \| \|
* \| \| \| \|	Port Lia.v	Chantal Keller	2021-05-26	1	-79/+127
\| \| \| \| \|
* \| \| \| \|	Minor changes on the Coq part	Chantal Keller	2021-05-26	4	-8/+6
\|/ / / /
* \| \| \|	Merge branch 'coq-8.11' of github.com:smtcoq/smtcoq into coq-8.12	Chantal Keller	2021-05-26	117	-117/+117
\|\\| \| \|
\| * \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-26	117	-117/+117
\| \|\\| \|
\| \| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-26	117	-117/+117
\| \| \|\\|
\| \| \| *	Update copyright	Chantal Keller	2021-05-26	117	-117/+117
\| \| \| \|
* \| \| \|	Port ocaml part	Chantal Keller	2021-05-26	4	-8/+7
\| \| \| \|
* \| \| \|	Port the Coq part	Chantal Keller	2021-05-26	6	-130/+121
\|/ / /
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-25	7	-715/+648
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-25	7	-715/+648
\| \|\\|
\| \| *	CompDec clean-up (#93)	ckeller	2021-05-25	7	-715/+648
\| \| \| \| \| \| \| \| \|	Clean-up the definition of CompDec, leaving the required minimum (in particular for functional arrays)
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11pxtp21	Chantal Keller	2021-05-06	1	-0/+11
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-06	1	-0/+11
\| \|\\|
\| \| *	Another silent change of veriT...	Chantal Keller	2021-05-06	1	-0/+11
\| \| \|
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-06	1	-11/+1
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-06	1	-11/+1
\| \|\\|
\| \| *	Less instances needed for auto	Chantal Keller	2021-05-06	1	-11/+1
\| \| \|
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-05	2	-2/+1
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-05	2	-2/+1
\| \|\\|
\| \| *	CompDec on interpreted type	Chantal Keller	2021-05-05	2	-2/+1
\| \| \|
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-05-05	3	-3/+32
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-05-05	3	-3/+32
\| \|\\|
\| \| *	Reify applied polymorphic terms with compdec	Chantal Keller	2021-05-05	3	-3/+32
\| \| \|
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-28	3	-4/+18
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-28	3	-4/+18
\| \|\\|
\| \| *	Solve a bug when reifying under a binder	Chantal Keller	2021-04-28	3	-4/+18
\| \| \|
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-28	2	-3/+3
\|\\| \|
\| * \|	Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10	Chantal Keller	2021-04-28	2	-3/+3
\| \|\\|
\| \| *	prop2bool_hyps insensitive to parenthesis	Chantal Keller	2021-04-28	2	-3/+3
\| \| \|
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	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	2	-4/+53
\| \|\\|
\| \| *	Equality between Booleans should be changed for hypotheses	Chantal Keller	2021-04-26	2	-4/+53
\| \| \|
* \| \|	Merge branch 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	1	-14/+17
\|\\| \|
\| * \|	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 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-26	4	-28/+190
\|\\| \|
\| * \|	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 'coq-8.10' of github.com:smtcoq/smtcoq into coq-8.11	Chantal Keller	2021-04-21	1	-15/+15
\|\\| \|