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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Merge remote-tracking branch 'smtcoq/master' into coq-8.10	vblot	2021-09-08	1	-9/+12
\|\
\| *	generalize polymorphic arguments detection	vblot	2021-09-08	1	-9/+12
\| \|
* \|	Rename directory because MacOS FS is case-insensitive	Chantal Keller	2021-08-30	3	-3/+3
\| \|
* \|	Merge remote-tracking branch 'origin/master' into HEAD	vblot	2021-08-25	2	-1/+3
\|\\|
\| *	fix array notations clash with ssreflect	vblot	2021-08-25	2	-1/+3
\| \|
* \|	Merge remote-tracking branch 'remotes/origin/master' into coq-8.10	Chantal Keller	2021-07-11	1	-58/+63
\|\\|
\| *	The verit tactics now immediately fail if veriT is not installed	Chantal Keller	2021-07-11	1	-58/+63
\| \|
* \|	use native integers (#96)	vblot	2021-07-07	25	-5042/+1664
\| \|
* \|	Merge remote-tracking branch 'remotes/origin/master' into coq-8.10	Chantal Keller	2021-06-02	3	-32/+117
\|\\|
\| *	Type back in CompDec (for efficiency reasons)	Chantal Keller	2021-06-02	3	-32/+117
\| \|
* \|	Add Makefile	Chantal Keller	2021-05-28	1	-0/+801
\| \|
* \|	getting rid of native-coq (#95)	vblot	2021-05-28	55	-2105/+804
\| \|
* \|	Get rid of most of our copy of micromega's source code (#94)	vblot	2021-05-28	5	-179/+10
\| \|
* \|	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
\| \|
* \|	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 '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 '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 '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 '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 '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 '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 '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 '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