aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrdersAlt.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* CompSpecType, a clone of CompSpec but in Type instead of PropGravatar letouzey2010-02-12
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07