| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Case1.v | 41 | logplain |
| -rw-r--r-- | Case10.v | 57 | logplain |
| -rw-r--r-- | Case11.v | 59 | logplain |
| -rw-r--r-- | Case12.v | 202 | logplain |
| -rw-r--r-- | Case13.v | 205 | logplain |
| -rw-r--r-- | Case14.v | 220 | logplain |
| -rw-r--r-- | Case2.v | 301 | logplain |
| -rw-r--r-- | Case3.v | 224 | logplain |
| -rw-r--r-- | Case4.v | 139 | logplain |
| -rw-r--r-- | Case5.v | 88 | logplain |
| -rw-r--r-- | Case6.v | 200 | logplain |
| -rw-r--r-- | Case7.v | 581 | logplain |
| -rw-r--r-- | Case8.v | 236 | logplain |
| -rw-r--r-- | Case9.v | 244 | logplain |
| -rw-r--r-- | ClearBody.v | 226 | logplain |
| -rw-r--r-- | Remark1.v | 76 | logplain |
| -rw-r--r-- | Remark2.v | 94 | logplain |
| -rw-r--r-- | Tauto.v | 883 | logplain |
| -rw-r--r-- | check.v | 35 | logplain |
| -rw-r--r-- | clash_cons.v | 651 | logplain |
| -rw-r--r-- | fixpoint1.v | 612 | logplain |
| -rw-r--r-- | illtype1.v | 531 | logplain |
| -rw-r--r-- | params_ind.v | 90 | logplain |
| -rw-r--r-- | positivity.v | 557 | logplain |
| -rw-r--r-- | redef.v | 566 | logplain |
| -rw-r--r-- | search.v | 560 | logplain |
| -rw-r--r-- | universes-buraliforti.v | 6018 | logplain |
| -rw-r--r-- | universes-sections1.v | 200 | logplain |
| -rw-r--r-- | universes-sections2.v | 220 | logplain |
| -rw-r--r-- | universes.v | 103 | logplain |
| -rw-r--r-- | universes2.v | 126 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |