aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Structures
ModeNameSize
-rw-r--r--DecidableType.v4162logplain
-rw-r--r--DecidableTypeEx.v3170logplain
-rw-r--r--Equalities.v6828logplain
-rw-r--r--EqualitiesFacts.v5062logplain
-rw-r--r--GenericMinMax.v20234logplain
-rw-r--r--OrderedType.v14324logplain
-rw-r--r--OrderedTypeAlt.v2965logplain
-rw-r--r--OrderedTypeEx.v6804logplain
-rw-r--r--Orders.v5470logplain
-rw-r--r--OrdersAlt.v6826logplain
-rw-r--r--OrdersEx.v2884logplain
-rw-r--r--OrdersFacts.v7155logplain
-rw-r--r--OrdersLists.v7192logplain
-rw-r--r--OrdersTac.v9564logplain
-rw-r--r--vo.itarget214logplain