aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/Orders.v
Commit message (Expand)AuthorAge
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* CompareSpec: a slight generalization/reformulation of CompSpecGravatar letouzey2011-03-17
* Reverted 13293 commited mistakenly. Sorry for the noise.Gravatar herbelin2010-07-18
* Tentative de suppression de l'import automatique des hints et coercions.Gravatar herbelin2010-07-18
* Bool: iff lemmas about or, a reflect inductive, an is_true functionGravatar letouzey2010-07-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Uniformisation Sorting/Mergesort and Structures/OrdersGravatar letouzey2010-02-16
* Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders*Gravatar letouzey2010-01-07