aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
ModeNameSize
-rw-r--r--DecidableType.v4150logplain
-rw-r--r--DecidableTypeEx.v3158logplain
-rw-r--r--Equalities.v7305logplain
-rw-r--r--EqualitiesFacts.v4757logplain
-rw-r--r--GenericMinMax.v20158logplain
-rw-r--r--OrderedType.v14302logplain
-rw-r--r--OrderedTypeAlt.v2953logplain
-rw-r--r--OrderedTypeEx.v9120logplain
-rw-r--r--Orders.v9963logplain
-rw-r--r--OrdersAlt.v6792logplain
-rw-r--r--OrdersEx.v2831logplain
-rw-r--r--OrdersFacts.v7139logplain
-rw-r--r--OrdersLists.v7207logplain
-rw-r--r--OrdersTac.v9564logplain
-rw-r--r--vo.itarget214logplain