aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/MSets/MSetProperties.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_rightGravatar letouzey2011-10-14
* Made option "Automatic Introduction" active by default before too manyGravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* 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
* OrderedType2 : trivial lemmas are turned into tests for order.Gravatar letouzey2009-10-16
* MSets: a new generation of FSetsGravatar letouzey2009-10-13