aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures/OrderTac.v
Commit message (Expand)AuthorAge
* OrderedType2 : trivial lemmas are turned into tests for order.Gravatar letouzey2009-10-16
* Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSet...Gravatar letouzey2009-10-16