| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | AddProps.v | 1343 | logplain |
| -rw-r--r-- | Axioms.v | 1256 | logplain |
| -rw-r--r-- | Definitions.v | 486 | logplain |
| -rw-r--r-- | DiscrAxioms.v | 172 | logplain |
| -rw-r--r-- | DiscrProps.v | 206 | logplain |
| -rw-r--r-- | GeAxioms.v | 243 | logplain |
| -rw-r--r-- | GeProps.v | 0 | logplain |
| -rw-r--r-- | GtAxioms.v | 244 | logplain |
| -rw-r--r-- | GtProps.v | 0 | logplain |
| -rw-r--r-- | LeAxioms.v | 265 | logplain |
| -rw-r--r-- | LeProps.v | 2672 | logplain |
| -rw-r--r-- | LtProps.v | 1661 | logplain |
| -rw-r--r-- | Make | 217 | logplain |
| -rw-r--r-- | NSyntax.v | 876 | logplain |
| -rw-r--r-- | OppAxioms.v | 0 | logplain |
| -rw-r--r-- | OppProps.v | 0 | logplain |
| -rw-r--r-- | SubProps.v | 0 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |