| Commit message (Expand) | Author | Age |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Rename [Morphism] into [Proper] and [respect] into [proper] to comply | msozeau | 2009-04-21 |
* | Just export RelationClasses for [Equivalence] through Setoid. | msozeau | 2009-04-18 |
* | Getting rid of the previous implementation of setoid_rewrite which was | msozeau | 2009-01-18 |
* | FMaps: various updates (mostly suggested by P. Casteran) | letouzey | 2008-12-26 |
* | Improve typeclasses eauto using the dnet for local assumptions too, and select | msozeau | 2008-09-04 |
* | - A little cleanup in Classes/*. Separate standard morphisms on | msozeau | 2008-04-08 |
* | Compatibility fixes, backtrack on definitions of reflexive, | msozeau | 2008-03-22 |
* | Plug the new setoid implemtation in, leaving the original one commented | msozeau | 2008-03-06 |
* | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau | 2007-12-31 |
* | Oubli dans Setoid.v | notin | 2007-09-28 |
* | Découpage de Setoid.v | notin | 2007-09-27 |
* | Mise en forme des theories | notin | 2006-10-17 |
* | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras | 2006-09-26 |
* | - Déplacement des types paramétriques prod, sum, option, identity, | herbelin | 2006-05-28 |
* | Duplication du fichier FSetProperties pour les ensembles Weak. | letouzey | 2006-05-11 |
* | Suppression des fichiers .cvsignore, rendus obsolètes par le systèmes des '... | notin | 2006-04-28 |
* | Minimum pour documentation TeX de la biblio | herbelin | 2006-02-22 |
* | Copy of the definition of prodT (already in the standard library) removed. | sacerdot | 2004-11-16 |
* | Proof term size reduction (again). | sacerdot | 2004-10-19 |
* | * Code simplification and clean-up. In particular there is no more code | sacerdot | 2004-10-18 |
* | iff and impl are now declared as transitive relations. | sacerdot | 2004-10-07 |
* | * New syntactic sugar: Add Relation ... transitivity proved by ... | sacerdot | 2004-10-06 |
* | added transitivity | barras | 2004-10-06 |
* | 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-29 |
* | * cleaning/renaming | sacerdot | 2004-09-08 |
* | The Coq part of the reflexive tactic is now able to handle also | sacerdot | 2004-09-08 |
* | * The Coq part of the reflexive tactic setoid_rewrite is generalized to | sacerdot | 2004-09-07 |
* | New reflexive implementation of setoid_rewrite. The new implementation | sacerdot | 2004-09-03 |
* | Nouvelle en-tête | herbelin | 2004-07-16 |
* | Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ... | herbelin | 2003-11-29 |
* | Cacher les .v8 | herbelin | 2003-10-03 |
* | Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co... | herbelin | 2002-05-29 |
* | Uniformisation (Qed/Save et Implicits Arguments) | herbelin | 2002-04-17 |
* | MAJ des Id pour coqweb | herbelin | 2002-01-09 |
* | Deplacement des setoides. | clrenard | 2001-09-19 |