| Age | Commit message (Expand) | Author |
|---|
| 2014-12-28 | Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ... | Arnaud Spiwack |
| 2014-12-18 | 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-11 | 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-08-05 | 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-05-06 | 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-02-07 | FinFun.v: results about injective/surjective/bijective fonctions over finite ... | Pierre Letouzey |
| 2013-12-20 | List: Bug 3039 weaker requirement for fold symmetric | Pierre Boutillier |
| 2013-07-24 | Added a concat function to List theory. Strangely, it was missing. | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-06-01 | list_eq_dec now transparent (wish #2786) | letouzey |
| 2012-05-18 | List + Permutation : more results about nth_error and nth | letouzey |
| 2011-09-02 | Bug 2589: Documentation patch of Hendrik Tews | pboutill |
| 2011-04-08 | A module out of Program to have list notations (bug 2463) | pboutill |
| 2010-12-17 | Cosmetic : let's take advantage of the n-ary exists notation | letouzey |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-07-22 | Made notations for exists, exists! and notations of Utf8.v recursive notations | herbelin |
| 2010-07-18 | 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-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-10 | Granting wish #2229 (InA_dec transparent) and Michael Day's coq-club | herbelin |
| 2010-02-17 | Arith's min and max placed in Peano (+basic specs max_l and co) | letouzey |
| 2009-12-13 | Addition of mergesort + cleaning of the Sorting library | herbelin |
| 2009-11-11 | Improving abbreviations/notations + backtrack of semantic change in r12439 | herbelin |
| 2009-11-02 | 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-10-29 | Fix flat_map definition so that it plays nicely with fix | glondu |
| 2009-10-13 | MSets: a new generation of FSets | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-08-19 | adds a property on map | bertot |
| 2009-08-19 | adds lemmas on interactions between existsb, forallb, and app | bertot |
| 2009-08-04 | - Add more precise error localisation when one of the application fails | herbelin |
| 2009-07-24 | List: add a iff-based lemma about In and ++ | letouzey |
| 2009-06-06 | Very-small-step policy changes to the library. | herbelin |
| 2008-08-06 | Add lemmas on lists: nth_default_eq, map_nth_error | glondu |
| 2008-05-27 | Cyclic31: migrate auxiliary lemmas to their legitimate files | letouzey |
| 2008-05-09 | Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ] | herbelin |
| 2008-04-29 | Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la | herbelin |
| 2008-04-28 | Backtrack on using metas eagerly in auto, only done in "new auto" for | msozeau |
| 2008-04-27 | - Fix bug in unification not taking into account the right meta | msozeau |
| 2008-04-08 | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau |
| 2008-04-01 | Correction du bug #1819 | notin |
