| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | DecidableType.v | 4562 | logplain |
| -rw-r--r-- | DecidableTypeEx.v | 3301 | logplain |
| -rw-r--r-- | Equalities.v | 8380 | logplain |
| -rw-r--r-- | EqualitiesFacts.v | 6476 | logplain |
| -rw-r--r-- | GenericMinMax.v | 19032 | logplain |
| -rw-r--r-- | OrderedType.v | 15840 | logplain |
| -rw-r--r-- | OrderedTypeAlt.v | 3110 | logplain |
| -rw-r--r-- | OrderedTypeEx.v | 15598 | logplain |
| -rw-r--r-- | Orders.v | 11107 | logplain |
| -rw-r--r-- | OrdersAlt.v | 6928 | logplain |
| -rw-r--r-- | OrdersEx.v | 4855 | logplain |
| -rw-r--r-- | OrdersFacts.v | 12880 | logplain |
| -rw-r--r-- | OrdersLists.v | 4948 | logplain |
| -rw-r--r-- | OrdersTac.v | 9421 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |