| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | .cvsignore | 5 | logplain |
| -rw-r--r-- | ArithRing.v | 2459 | logplain |
| -rw-r--r-- | NArithRing.v | 1380 | logplain |
| -rw-r--r-- | Quote.v | 2531 | logplain |
| -rw-r--r-- | Ring.v | 1400 | logplain |
| -rw-r--r-- | Ring_abstract.v | 20491 | logplain |
| -rw-r--r-- | Ring_normalize.v | 27344 | logplain |
| -rw-r--r-- | Ring_theory.v | 9770 | logplain |
| -rw-r--r-- | Setoid_ring.v | 633 | logplain |
| -rw-r--r-- | Setoid_ring_normalize.v | 40942 | logplain |
| -rw-r--r-- | Setoid_ring_theory.v | 10613 | logplain |
| -rw-r--r-- | ZArithRing.v | 1271 | logplain |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |