| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Cases.out | 859 | logplain |
| -rw-r--r-- | Cases.v | 685 | logplain |
| -rw-r--r-- | Coercions.out | 90 | logplain |
| -rw-r--r-- | Coercions.v | 413 | logplain |
| -rw-r--r-- | Fixpoint.out | 624 | logplain |
| -rw-r--r-- | Fixpoint.v | 899 | logplain |
| -rw-r--r-- | Implicit.out | 344 | logplain |
| -rw-r--r-- | Implicit.v | 947 | logplain |
| -rw-r--r-- | InitSyntax.out | 382 | logplain |
| -rw-r--r-- | InitSyntax.v | 111 | logplain |
| -rw-r--r-- | Intuition.out | 91 | logplain |
| -rw-r--r-- | Intuition.v | 121 | logplain |
| -rw-r--r-- | Nametab.out | 1096 | logplain |
| -rw-r--r-- | Nametab.v | 906 | logplain |
| -rw-r--r-- | Notations.out | 937 | logplain |
| -rw-r--r-- | Notations.v | 3718 | logplain |
| -rw-r--r-- | RealSyntax.out | 31 | logplain |
| -rw-r--r-- | RealSyntax.v | 49 | logplain |
| -rw-r--r-- | Sum.out | 99 | logplain |
| -rw-r--r-- | Sum.v | 93 | logplain |
| -rw-r--r-- | Tactics.out | 134 | logplain |
| -rw-r--r-- | Tactics.v | 488 | logplain |
| -rw-r--r-- | TranspModtype.out | 89 | logplain |
| -rw-r--r-- | TranspModtype.v | 385 | logplain |
| -rw-r--r-- | ZSyntax.out | 571 | logplain |
| -rw-r--r-- | ZSyntax.v | 558 | logplain |
| -rw-r--r-- | reduction.out | 44 | logplain |
| -rw-r--r-- | reduction.v | 280 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |