| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | BinInt.v | 52776 | logplain |
| -rw-r--r-- | BinIntDef.v | 16463 | logplain |
| -rw-r--r-- | Int.v | 15385 | logplain |
| -rw-r--r-- | Wf_Z.v | 6190 | logplain |
| -rw-r--r-- | ZArith.v | 986 | logplain |
| -rw-r--r-- | ZArith_base.v | 1452 | logplain |
| -rw-r--r-- | ZArith_dec.v | 4904 | logplain |
| -rw-r--r-- | Zabs.v | 3511 | logplain |
| -rw-r--r-- | Zbool.v | 5026 | logplain |
| -rw-r--r-- | Zcompare.v | 5338 | logplain |
| -rw-r--r-- | Zcomplements.v | 5432 | logplain |
| -rw-r--r-- | Zdigits.v | 8971 | logplain |
| -rw-r--r-- | Zdiv.v | 22167 | logplain |
| -rw-r--r-- | Zeuclid.v | 1884 | logplain |
| -rw-r--r-- | Zeven.v | 7936 | logplain |
| -rw-r--r-- | Zgcd_alt.v | 8683 | logplain |
| -rw-r--r-- | Zhints.v | 4066 | logplain |
| -rw-r--r-- | Zmax.v | 2127 | logplain |
| -rw-r--r-- | Zmin.v | 1897 | logplain |
| -rw-r--r-- | Zminmax.v | 1301 | logplain |
| -rw-r--r-- | Zmisc.v | 1227 | logplain |
| -rw-r--r-- | Znat.v | 28209 | logplain |
| -rw-r--r-- | Znumtheory.v | 29778 | logplain |
| -rw-r--r-- | Zorder.v | 15162 | logplain |
| -rw-r--r-- | Zpow_alt.v | 2711 | logplain |
| -rw-r--r-- | Zpow_def.v | 1482 | logplain |
| -rw-r--r-- | Zpow_facts.v | 7988 | logplain |
| -rw-r--r-- | Zpower.v | 10922 | logplain |
| -rw-r--r-- | Zquot.v | 13740 | logplain |
| -rw-r--r-- | Zwf.v | 2465 | logplain |
| -rw-r--r-- | auxiliary.v | 2880 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |