coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	List.nth_error directly produces Some/None instead of value/error	Pierre Letouzey	2015-05-12
*	Giving to "subst" a more natural semantic (fixing #4214) by using all	Hugo Herbelin	2015-05-01
*	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
*	Introducing MMaps, a modernized FMaps.	Pierre Letouzey	2015-03-04
*	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
*	Clarifying the role of ListSet.v in the library, compared to other	Hugo Herbelin	2014-11-18
*	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
*	More proofs independent of the names generated by induction/elim over	Hugo Herbelin	2014-08-05
*	Adding a generalized version of fold_Equal to FMapFacts.	Pierre Courtieu	2014-07-31
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04
*	Making those proofs which depend on names generated for the arguments	Hugo Herbelin	2014-06-01
*	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
*	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	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
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Updating headers.	herbelin	2012-08-08
*	isolate instances about Permutation and PermutationA which may slow rewrite	letouzey	2012-07-10
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	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
*	SetoidList: explicit the fact that InfA_compat won't use ltA_strorder	letouzey	2012-05-22
*	List + Permutation : more results about nth_error and nth	letouzey	2012-05-18
*	A notion of permutation for lists modulo a setoid equality	letouzey	2012-05-02
*	Uniformisation in the documentation: remove the use of 'coinductive' in	aspiwack	2012-04-13
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Bug 2589: Documentation patch of Hendrik Tews	pboutill	2011-09-02
*	A module out of Program to have list notations (bug 2463)	pboutill	2011-04-08
*	Simplify proofs in Permutation using generalized rewriting.	msozeau	2011-03-04
*	Remove obsolete TheoryList	glondu	2011-02-10
*	Cosmetic : let's take advantage of the n-ary exists notation	letouzey	2010-12-17
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin	2010-07-22
*	Reverted 13293 commited mistakenly. Sorry for the noise.	herbelin	2010-07-18
*	Tentative de suppression de l'import automatique des hints et coercions.	herbelin	2010-07-18
*	Fixing definition of set_map (bug report #2111) which was actually already	herbelin	2010-06-13
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29