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