coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
*	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
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Granting wish #2229 (InA_dec transparent) and Michael Day's coq-club	herbelin	2010-04-10
*	Arith's min and max placed in Peano (+basic specs max_l and co)	letouzey	2010-02-17
*	Addition of mergesort + cleaning of the Sorting library	herbelin	2009-12-13
*	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin	2009-11-11
*	List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F...	letouzey	2009-11-02
*	Remove various useless {struct} annotations	letouzey	2009-11-02
*	list, length, app are migrated from List to Datatypes	letouzey	2009-11-02
*	Fix flat_map definition so that it plays nicely with fix	glondu	2009-10-29
*	MSets: a new generation of FSets	letouzey	2009-10-13
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	adds a property on map	bertot	2009-08-19
*	adds lemmas on interactions between existsb, forallb, and app	bertot	2009-08-19
*	- Add more precise error localisation when one of the application fails	herbelin	2009-08-04
*	List: add a iff-based lemma about In and ++	letouzey	2009-07-24
*	Very-small-step policy changes to the library.	herbelin	2009-06-06
*	Add lemmas on lists: nth_default_eq, map_nth_error	glondu	2008-08-06
*	Cyclic31: migrate auxiliary lemmas to their legitimate files	letouzey	2008-05-27
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	Backtrack on using metas eagerly in auto, only done in "new auto" for	msozeau	2008-04-28
*	- Fix bug in unification not taking into account the right meta	msozeau	2008-04-27
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08