| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | CEquivalence.v | 4979 | logplain |
| -rw-r--r-- | CMorphisms.v | 22820 | logplain |
| -rw-r--r-- | CRelationClasses.v | 12930 | logplain |
| -rw-r--r-- | DecidableClass.v | 3146 | logplain |
| -rw-r--r-- | EquivDec.v | 4613 | logplain |
| -rw-r--r-- | Equivalence.v | 4989 | logplain |
| -rw-r--r-- | Init.v | 1608 | logplain |
| -rw-r--r-- | Morphisms.v | 22654 | logplain |
| -rw-r--r-- | Morphisms_Prop.v | 3382 | logplain |
| -rw-r--r-- | Morphisms_Relations.v | 2546 | logplain |
| -rw-r--r-- | RelationClasses.v | 17097 | logplain |
| -rw-r--r-- | RelationPairs.v | 5290 | logplain |
| -rw-r--r-- | SetoidClass.v | 4656 | logplain |
| -rw-r--r-- | SetoidDec.v | 3926 | logplain |
| -rw-r--r-- | SetoidTactics.v | 6292 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |