aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/Orders.v
Commit message (Expand)AuthorAge
* 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