| Age | Commit message (Expand) | Author |
| 2020-10-02 | {new,setoid_}ring -> ring | Maxime Dénès |
| 2020-08-25 | Modify Setoids/Setoid.v to compile with -mangle-names | Jasper Hugunin |
| 2020-03-18 | Update headers in the whole code base. | Théo Zimmermann |
| 2019-08-08 | [ssr] Refactor under's Setoid generalization to ease stdlib2 porting | Erik Martin-Dorel |
| 2019-06-17 | Update ml-style headers to new year. | Théo Zimmermann |
| 2018-10-10 | [coqlib] Rebindable Coqlib namespace. | Emilio Jesus Gallego Arias |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-09-17 | Add some missing Proof statements. | Guillaume Melquiond |
| 2012-08-08 | Updating headers. | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-08 | Made option "Automatic Introduction" active by default before too many | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-04-21 | Rename [Morphism] into [Proper] and [respect] into [proper] to comply | msozeau |
| 2009-04-18 | Just export RelationClasses for [Equivalence] through Setoid. | msozeau |
| 2008-12-26 | FMaps: various updates (mostly suggested by P. Casteran) | letouzey |
| 2008-09-04 | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau |
| 2008-04-08 | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau |
| 2008-03-22 | Compatibility fixes, backtrack on definitions of reflexive, | msozeau |
| 2008-03-06 | Plug the new setoid implemtation in, leaving the original one commented | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-09-28 | Oubli dans Setoid.v | notin |
| 2007-09-27 | Découpage de Setoid.v | notin |
| 2006-10-17 | Mise en forme des theories | notin |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2006-05-28 | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin |
| 2006-05-11 | Duplication du fichier FSetProperties pour les ensembles Weak. | letouzey |
| 2004-11-16 | Copy of the definition of prodT (already in the standard library) removed. | sacerdot |
| 2004-10-19 | Proof term size reduction (again). | sacerdot |
| 2004-10-18 | * Code simplification and clean-up. In particular there is no more code | sacerdot |
| 2004-10-07 | iff and impl are now declared as transitive relations. | sacerdot |
| 2004-10-06 | * New syntactic sugar: Add Relation ... transitivity proved by ... | sacerdot |
| 2004-10-06 | added transitivity | barras |
| 2004-09-29 | impl is a reflexive relation (it used to be areflexive). | sacerdot |
| 2004-09-29 | impl relation and impl/and/or/not morphisms over impl declared. | sacerdot |
| 2004-09-08 | * cleaning/renaming | sacerdot |
| 2004-09-08 | The Coq part of the reflexive tactic is now able to handle also | sacerdot |
| 2004-09-07 | * The Coq part of the reflexive tactic setoid_rewrite is generalized to | sacerdot |
| 2004-09-03 | New reflexive implementation of setoid_rewrite. The new implementation | sacerdot |
| 2004-07-16 | Nouvelle en-tête | herbelin |
| 2003-11-29 | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin |
| 2002-05-29 | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin |
| 2002-04-17 | Uniformisation (Qed/Save et Implicits Arguments) | herbelin |
| 2002-01-09 | MAJ des Id pour coqweb | herbelin |
| 2001-09-19 | Deplacement des setoides. | clrenard |