| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | Algebra_syntax.v | 1599 | logplain |
| -rw-r--r-- | ArithRing.v | 2283 | logplain |
| -rw-r--r-- | BinList.v | 2509 | logplain |
| -rw-r--r-- | Cring.v | 9160 | logplain |
| -rw-r--r-- | Field.v | 731 | logplain |
| -rw-r--r-- | Field_tac.v | 19725 | logplain |
| -rw-r--r-- | Field_theory.v | 56503 | logplain |
| -rw-r--r-- | InitialRing.v | 27244 | logplain |
| -rw-r--r-- | Integral_domain.v | 1980 | logplain |
| -rw-r--r-- | NArithRing.v | 919 | logplain |
| -rw-r--r-- | Ncring.v | 9630 | logplain |
| -rw-r--r-- | Ncring_initial.v | 6378 | logplain |
| -rw-r--r-- | Ncring_polynom.v | 17167 | logplain |
| -rw-r--r-- | Ncring_tac.v | 9751 | logplain |
| -rw-r--r-- | RealField.v | 4318 | logplain |
| -rw-r--r-- | Ring.v | 1702 | logplain |
| -rw-r--r-- | Ring_base.v | 942 | logplain |
| -rw-r--r-- | Ring_polynom.v | 44895 | logplain |
| -rw-r--r-- | Ring_tac.v | 15703 | logplain |
| -rw-r--r-- | Ring_theory.v | 19211 | logplain |
| -rw-r--r-- | Rings_Q.v | 1464 | logplain |
| -rw-r--r-- | Rings_R.v | 1604 | logplain |
| -rw-r--r-- | Rings_Z.v | 995 | logplain |
| -rw-r--r-- | ZArithRing.v | 1692 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |