| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | EquivDec.v | 4614 | logplain |
| -rw-r--r-- | Equivalence.v | 4218 | logplain |
| -rw-r--r-- | Functions.v | 1544 | logplain |
| -rw-r--r-- | Init.v | 1480 | logplain |
| -rw-r--r-- | Morphisms.v | 15565 | logplain |
| -rw-r--r-- | Morphisms_Prop.v | 3122 | logplain |
| -rw-r--r-- | Morphisms_Relations.v | 2395 | logplain |
| -rw-r--r-- | RelationClasses.v | 13102 | logplain |
| -rw-r--r-- | SetoidAxioms.v | 1262 | logplain |
| -rw-r--r-- | SetoidClass.v | 4934 | logplain |
| -rw-r--r-- | SetoidDec.v | 3769 | logplain |
| -rw-r--r-- | SetoidTactics.v | 6597 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |