coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\
* \|	Remove VOld compatibility flag.	Théo Zimmermann	2018-03-02
\| *	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|/
*	Make list functions returning sumbools transparent	Tej Chajed	2017-11-15
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Fix 3 unused-intro-pattern warnings in stdlib.	Théo Zimmermann	2017-03-14
*	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
*	Move vector/list compat notations to their relevant files	Jason Gross	2016-09-29
*	Remove spaces from around list notations	Jason Gross	2016-09-26
*	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
*	Revert "Temporary hack to compensate missing comma while re-printing tactic"	Hugo Herbelin	2016-04-27
*	Temporary hack to compensate missing comma while re-printing tactic	Hugo Herbelin	2016-04-27
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-02-21
\|\
\| *	Fixing bug #4582: cannot override notation [ x ].	Pierre-Marie Pédrot	2016-02-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-17
\|\\|
\| *	Proof using: do not clear unused section hyps automatically	Enrico Tassi	2015-12-15
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-14
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
\| *	List.nth_error directly produces Some/None instead of value/error	Pierre Letouzey	2015-05-12
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Giving to "subst" a more natural semantic (fixing #4214) by using all	Hugo Herbelin	2015-05-01
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Prove [map_ext] using [map_ext_in].	Nickolai Zeldovich	2015-04-09
\| *	Add a [map_ext_in] lemma to List.v.	Nickolai Zeldovich	2015-04-09
* \|	Add two lemmas about firstn to the List standard library.	Sébastien Hinderer	2015-01-16
* \|	Lemmas related to the firstn function over lists.	Sébastien Hinderer	2015-01-16
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...	Arnaud Spiwack	2014-12-28
*	Adds two lemmas about hderror to the List standard library.	Sébastien Hinderer	2014-12-18
*	Implement the nodup function on lists and prove associated results.	Sébastien Hinderer	2014-12-18
*	Lists: enhanced version of Seb's last commit on Exists/Forall	Pierre Letouzey	2014-12-18
*	Lists: a few results on Exists and Forall and a bit of code cleanup.	Sébastien Hinderer	2014-12-18
*	List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)	Pierre Letouzey	2014-12-11
*	First series of results on lists.	Sébastien Hinderer	2014-12-11
*	Improving printing of "[]" (nil) in spite of the risk of collision	Hugo Herbelin	2014-08-05
*	Testing a replacement of "cut" by "enough" on a couple of test files.	Hugo Herbelin	2014-08-05
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	FinFun.v: results about injective/surjective/bijective fonctions over finite ...	Pierre Letouzey	2014-02-07
*	List: Bug 3039 weaker requirement for fold symmetric	Pierre Boutillier	2013-12-20
*	Added a concat function to List theory. Strangely, it was missing.	ppedrot	2013-07-24
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	list_eq_dec now transparent (wish #2786)	letouzey	2012-06-01
*	List + Permutation : more results about nth_error and nth	letouzey	2012-05-18