aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
ModeNameSize
-rw-r--r--DecidableType.v4152logplain
-rw-r--r--DecidableTypeEx.v3144logplain
-rw-r--r--Equalities.v8172logplain
-rw-r--r--EqualitiesFacts.v5886logplain
-rw-r--r--GenericMinMax.v18792logplain
-rw-r--r--OrderedType.v14386logplain
-rw-r--r--OrderedTypeAlt.v2953logplain
-rw-r--r--OrderedTypeEx.v8534logplain
-rw-r--r--Orders.v10805logplain
-rw-r--r--OrdersAlt.v6771logplain
-rw-r--r--OrdersEx.v4593logplain
-rw-r--r--OrdersFacts.v12744logplain
-rw-r--r--OrdersLists.v4621logplain
-rw-r--r--OrdersTac.v9285logplain
-rw-r--r--vo.itarget214logplain