| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | DecidableType.v | 4065 | logplain |
| -rw-r--r-- | DecidableType2.v | 3898 | logplain |
| -rw-r--r-- | DecidableType2Ex.v | 1723 | logplain |
| -rw-r--r-- | DecidableType2Facts.v | 3734 | logplain |
| -rw-r--r-- | DecidableTypeEx.v | 3465 | logplain |
| -rw-r--r-- | GenericMinMax.v | 15361 | logplain |
| -rw-r--r-- | OrderTac.v | 8907 | logplain |
| -rw-r--r-- | OrderedType.v | 14479 | logplain |
| -rw-r--r-- | OrderedType2.v | 2872 | logplain |
| -rw-r--r-- | OrderedType2Alt.v | 6807 | logplain |
| -rw-r--r-- | OrderedType2Ex.v | 2844 | logplain |
| -rw-r--r-- | OrderedType2Facts.v | 8056 | logplain |
| -rw-r--r-- | OrderedType2Lists.v | 7678 | logplain |
| -rw-r--r-- | OrderedTypeAlt.v | 2965 | logplain |
| -rw-r--r-- | OrderedTypeEx.v | 6804 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |