| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | .cvsignore | 5 | logplain |
| -rw-r--r-- | .depend | 2996 | logplain |
| -rw-r--r-- | AddProps.v | 1609 | logplain |
| -rw-r--r-- | Axioms.v | 1497 | logplain |
| -rw-r--r-- | Definitions.v | 1009 | logplain |
| -rw-r--r-- | DiscrAxioms.v | 698 | logplain |
| -rw-r--r-- | DiscrProps.v | 731 | logplain |
| -rw-r--r-- | EqAxioms.v | 1178 | logplain |
| -rw-r--r-- | EqParams.v | 925 | logplain |
| -rw-r--r-- | GeAxioms.v | 770 | logplain |
| -rw-r--r-- | GeProps.v | 525 | logplain |
| -rw-r--r-- | GtAxioms.v | 770 | logplain |
| -rw-r--r-- | GtProps.v | 525 | logplain |
| -rw-r--r-- | LeAxioms.v | 792 | logplain |
| -rw-r--r-- | LeProps.v | 3183 | logplain |
| d--------- | Leibniz | 178 | logplain |
| -rw-r--r-- | LtProps.v | 2200 | logplain |
| -rw-r--r-- | Make | 253 | logplain |
| -rw-r--r-- | Makefile | 6754 | logplain |
| -rw-r--r-- | NSyntax.v | 1214 | logplain |
| d--------- | Nat | 176 | logplain |
| -rw-r--r-- | NeqAxioms.v | 966 | logplain |
| -rw-r--r-- | NeqDef.v | 1097 | logplain |
| -rw-r--r-- | NeqParams.v | 754 | logplain |
| -rw-r--r-- | NeqProps.v | 1453 | logplain |
| -rw-r--r-- | OppAxioms.v | 525 | logplain |
| -rw-r--r-- | OppProps.v | 525 | logplain |
| -rw-r--r-- | Params.v | 999 | logplain |
| -rw-r--r-- | SubProps.v | 525 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |