| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | BinInt.v | 52958 | logplain |
| -rw-r--r-- | BinIntDef.v | 16482 | logplain |
| -rw-r--r-- | Int.v | 15385 | logplain |
| -rw-r--r-- | Wf_Z.v | 6246 | logplain |
| -rw-r--r-- | ZArith.v | 986 | logplain |
| -rw-r--r-- | ZArith_base.v | 1462 | logplain |
| -rw-r--r-- | ZArith_dec.v | 4882 | logplain |
| -rw-r--r-- | Zabs.v | 3533 | logplain |
| -rw-r--r-- | Zbool.v | 5026 | logplain |
| -rw-r--r-- | Zcompare.v | 5338 | logplain |
| -rw-r--r-- | Zcomplements.v | 5496 | logplain |
| -rw-r--r-- | Zdigits.v | 8971 | logplain |
| -rw-r--r-- | Zdiv.v | 22403 | logplain |
| -rw-r--r-- | Zeuclid.v | 1884 | logplain |
| -rw-r--r-- | Zeven.v | 7946 | logplain |
| -rw-r--r-- | Zgcd_alt.v | 8683 | logplain |
| -rw-r--r-- | Zhints.v | 4076 | 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 | 28227 | logplain |
| -rw-r--r-- | Znumtheory.v | 30215 | logplain |
| -rw-r--r-- | Zorder.v | 15232 | logplain |
| -rw-r--r-- | Zpow_alt.v | 2711 | logplain |
| -rw-r--r-- | Zpow_def.v | 1512 | logplain |
| -rw-r--r-- | Zpow_facts.v | 7998 | logplain |
| -rw-r--r-- | Zpower.v | 10962 | logplain |
| -rw-r--r-- | Zquot.v | 13750 | logplain |
| -rw-r--r-- | Zwf.v | 2485 | logplain |
| -rw-r--r-- | auxiliary.v | 2880 | logplain |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |