aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/DecidableType.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Stop using auto with * in two proofs.Gravatar Théo Zimmermann2017-05-16
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Merge SetoidList2 into SetoidList.Gravatar letouzey2009-10-19
* MSets: a new generation of FSetsGravatar letouzey2009-10-13