| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Cases.out | 196 | logplain |
| -rw-r--r-- | Cases.v | 101 | logplain |
| -rw-r--r-- | Coercions.out | 81 | logplain |
| -rw-r--r-- | Coercions.v | 390 | logplain |
| -rw-r--r-- | Fixpoint.v | 166 | logplain |
| -rw-r--r-- | Implicit.out | 125 | logplain |
| -rw-r--r-- | Implicit.v | 586 | logplain |
| -rw-r--r-- | InitSyntax.out | 179 | logplain |
| -rw-r--r-- | InitSyntax.v | 93 | logplain |
| -rw-r--r-- | Intuition.out | 87 | logplain |
| -rw-r--r-- | Intuition.v | 100 | logplain |
| -rw-r--r-- | Notations.out8 | 350 | logplain |
| -rw-r--r-- | Notations.v8 | 567 | logplain |
| -rw-r--r-- | RealSyntax.out | 33 | logplain |
| -rw-r--r-- | RealSyntax.v | 44 | logplain |
| -rw-r--r-- | Sum.out | 87 | logplain |
| -rw-r--r-- | Sum.v | 75 | logplain |
| -rw-r--r-- | TranspModtype.out | 92 | logplain |
| -rw-r--r-- | TranspModtype.v | 363 | logplain |
| -rw-r--r-- | ZSyntax.out | 518 | logplain |
| -rw-r--r-- | ZSyntax.v | 488 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |