| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Demo.v | 616 | logplain |
| -rw-r--r-- | Nat.v | 315 | logplain |
| -rw-r--r-- | PO.v | 1138 | logplain |
| -rw-r--r-- | Przyklad.v | 3817 | logplain |
| -rw-r--r-- | SeveralWith.v | 211 | logplain |
| -rw-r--r-- | Tescik.v | 568 | logplain |
| -rw-r--r-- | WithDefUBinders.v | 414 | logplain |
| -rw-r--r-- | cumpoly.v | 614 | logplain |
| -rw-r--r-- | errors.v | 2980 | logplain |
| -rw-r--r-- | fun_objects.v | 432 | logplain |
| -rw-r--r-- | grammar.v | 239 | logplain |
| -rw-r--r-- | ind.v | 1322 | logplain |
| -rw-r--r-- | injection_discriminate_inversion.v | 611 | logplain |
| -rw-r--r-- | mod_decl.v | 543 | logplain |
| -rw-r--r-- | modeq.v | 322 | logplain |
| -rw-r--r-- | modul.v | 394 | logplain |
| -rw-r--r-- | nested_mod_types.v | 389 | logplain |
| -rw-r--r-- | obj.v | 386 | logplain |
| -rw-r--r-- | objects.v | 402 | logplain |
| -rw-r--r-- | objects2.v | 384 | logplain |
| -rw-r--r-- | pliczek.v | 59 | logplain |
| -rw-r--r-- | plik.v | 83 | logplain |
| -rw-r--r-- | polymorphism.v | 1059 | logplain |
| -rw-r--r-- | polymorphism2.v | 1050 | logplain |
| -rw-r--r-- | pseudo_circular_with.v | 156 | logplain |
| -rw-r--r-- | resolver.v | 466 | logplain |
| -rw-r--r-- | sig.v | 431 | logplain |
| -rw-r--r-- | sub_objects.v | 600 | logplain |
| -rw-r--r-- | subtyping.v | 1373 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |