| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Coercions.out | 38 | logplain |
| -rw-r--r-- | Coercions.v | 245 | logplain |
| -rw-r--r-- | InitSyntax.out | 108 | logplain |
| -rw-r--r-- | InitSyntax.v | 37 | logplain |
| -rw-r--r-- | Intuition.out | 87 | logplain |
| -rw-r--r-- | Intuition.v | 93 | logplain |
| -rw-r--r-- | Nametab.out | 586 | logplain |
| -rw-r--r-- | Nametab.v | 779 | logplain |
| -rw-r--r-- | RealSyntax.out | 33 | logplain |
| -rw-r--r-- | RealSyntax.v | 44 | logplain |
| -rw-r--r-- | Remark2.out | 30 | logplain |
| -rw-r--r-- | Remark2.v | 94 | logplain |
| -rw-r--r-- | Sum.out | 87 | logplain |
| -rw-r--r-- | Sum.v | 75 | logplain |
| -rw-r--r-- | ZSyntax.out | 518 | logplain |
| -rw-r--r-- | ZSyntax.v | 488 | logplain |
| -rw-r--r-- | implicits.out | 107 | logplain |
| -rw-r--r-- | implicits.v | 460 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |