| Age | Commit message (Expand) | Author |
| 2021-01-08 | Modify Lists/SetoidList.v to compile with -mangle-names | Jasper Hugunin |
| 2020-11-16 | Explicitly annotate all hint declarations of the standard library. | Pierre-Marie Pédrot |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2018-11-14 | Deprecate hint declaration/removal with no specified database | Maxime Dénès |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2015-03-04 | Introducing MMaps, a modernized FMaps. | Pierre Letouzey |
| 2014-07-31 | Adding a generalized version of fold_Equal to FMapFacts. | Pierre Courtieu |
| 2014-06-26 | Avoid using a deprecated lemma in the standard library. | Guillaume Melquiond |
| 2014-06-01 | Making those proofs which depend on names generated for the arguments | Hugo Herbelin |
| 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 |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-07-10 | isolate instances about Permutation and PermutationA which may slow rewrite | letouzey |
| 2012-05-22 | SetoidList: explicit the fact that InfA_compat won't use ltA_strorder | letouzey |
| 2012-05-02 | A notion of permutation for lists modulo a setoid equality | letouzey |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-03-04 | Simplify proofs in Permutation using generalized rewriting. | msozeau |
| 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 |
| 2009-11-02 | List + SetoidList : some cleanup around predicates Exists, Forall, Forall2, F... | letouzey |
| 2009-10-19 | Merge SetoidList2 into SetoidList. | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-07-20 | Typo in a comment | letouzey |
| 2009-01-18 | Various little fixes: | msozeau |
| 2008-12-26 | FMaps: various updates (mostly suggested by P. Casteran) | letouzey |
| 2008-12-22 | FMap: fold_rec + more permissive transpose hyp + various cleanup | letouzey |
| 2008-03-04 | migration from Set to Type of FSet/FMap + some dependencies... | letouzey |
| 2007-11-06 | small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is | letouzey |
| 2007-06-27 | - Extensions of FMap(Weak)Facts: | letouzey |
| 2007-06-26 | additional properties for FMap (and slight rework of SetoidList and FSetPrope... | letouzey |
| 2007-06-14 | oups: one file forgotten in my previous commit | letouzey |
| 2007-06-08 | some more properties of fold and elements in FSetProperties | letouzey |
| 2006-05-23 | Changement de précédence de l'argument du by de assert; conséquences... | herbelin |
| 2006-05-22 | un debut de propriétés concernant FMap | letouzey |
| 2006-05-15 | petit ajout concernant InA | letouzey |
| 2006-05-11 | decidabilite de InA | letouzey |
| 2006-05-11 | Duplication du fichier FSetProperties pour les ensembles Weak. | letouzey |
| 2006-04-06 | versement de MoreList.v dans List.v, reorganisation, quelques nouveaux lemmes | letouzey |
| 2006-03-16 | propriete svn:keywords positionnee a Author Date Id Revision sur l'ensemble d... | letouzey |
| 2006-03-16 | utilisation de removeA dans FSetProperties | letouzey |
| 2006-03-15 | renommage NoRedun vers le plus joli NoDup | letouzey |
| 2006-03-15 | Typo | letouzey |
| 2006-03-15 | Ajout de fonctions sur les listes | notin |
| 2006-03-15 | Ajout de theories/FSets contenant la partie "light" de FSets et FMap: | letouzey |