aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetEqProperties.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Avoid declaring hints about refl/sym/trans of eq in DecidableType2Gravatar letouzey2010-01-05
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* MSets: a new generation of FSetsGravatar letouzey2009-10-13