| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | 1338.v-disabled | 332 | logplain |
| -rw-r--r-- | 1501.v | 2587 | logplain |
| -rw-r--r-- | 1596.v | 7383 | logplain |
| -rw-r--r-- | 1671.v | 322 | logplain |
| -rw-r--r-- | 1811.v | 200 | logplain |
| -rw-r--r-- | 3230.v | 372 | logplain |
| -rw-r--r-- | 3263.v | 9733 | logplain |
| -rw-r--r-- | 3277.v | 188 | logplain |
| -rw-r--r-- | 3278.v | 633 | logplain |
| -rw-r--r-- | 3283.v | 1019 | logplain |
| -rw-r--r-- | 3295.v | 3057 | logplain |
| -rw-r--r-- | 3298.v | 508 | logplain |
| -rw-r--r-- | 3304.v | 203 | logplain |
| -rw-r--r-- | 3311.v | 337 | logplain |
| -rw-r--r-- | 3312.v | 185 | logplain |
| -rw-r--r-- | 3326.v | 384 | logplain |
| -rw-r--r-- | 3343.v | 1296 | logplain |
| -rw-r--r-- | 3345.v | 5372 | logplain |
| -rw-r--r-- | 3357.v | 321 | logplain |
| -rw-r--r-- | 3363.v | 479 | logplain |
| -rw-r--r-- | 3370.v | 341 | logplain |
| -rw-r--r-- | 3383.v | 506 | logplain |
| -rw-r--r-- | 3388.v | 1295 | logplain |
| -rw-r--r-- | 3395.v | 9693 | logplain |
| -rw-r--r-- | 3459.v | 302 | logplain |
| -rw-r--r-- | 3509.v | 528 | logplain |
| -rw-r--r-- | 3510.v | 1142 | logplain |
| -rw-r--r-- | 3554.v | 50 | logplain |
| -rw-r--r-- | 3562.v | 34 | logplain |
| -rw-r--r-- | 3566.v | 1077 | logplain |
| -rw-r--r-- | 3618.v | 3602 | logplain |
| -rw-r--r-- | 3625.v | 179 | logplain |
| -rw-r--r-- | 3626.v | 179 | logplain |
| -rw-r--r-- | 3628.v | 191 | logplain |
| -rw-r--r-- | 3655.v | 122 | logplain |
| -rw-r--r-- | 3657.v | 728 | logplain |
| -rw-r--r-- | 3660.v | 1219 | logplain |
| -rw-r--r-- | 743.v | 218 | logplain |
| -rw-r--r-- | HoTT_coq_106.v | 2002 | logplain |
| -rw-r--r-- | HoTT_coq_120.v | 5392 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |