aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith
ModeNameSize
-rw-r--r--BinInt.v52387logplain
-rw-r--r--BinIntDef.v14865logplain
-rw-r--r--Int.v15202logplain
-rw-r--r--Wf_Z.v6040logplain
-rw-r--r--ZArith.v841logplain
-rw-r--r--ZArith_base.v1302logplain
-rw-r--r--ZArith_dec.v4801logplain
-rw-r--r--Zabs.v3577logplain
-rw-r--r--Zbool.v4876logplain
-rw-r--r--Zcompare.v5519logplain
-rw-r--r--Zcomplements.v4740logplain
-rw-r--r--Zdigits.v8858logplain
-rw-r--r--Zdiv.v21420logplain
-rw-r--r--Zeuclid.v1734logplain
-rw-r--r--Zeven.v7871logplain
-rw-r--r--Zgcd_alt.v9209logplain
-rw-r--r--Zhints.v3916logplain
-rw-r--r--Zlogarithm.v8438logplain
-rw-r--r--Zmax.v2448logplain
-rw-r--r--Zmin.v2218logplain
-rw-r--r--Zminmax.v1151logplain
-rw-r--r--Zmisc.v1077logplain
-rw-r--r--Znat.v27563logplain
-rw-r--r--Znumtheory.v26686logplain
-rw-r--r--Zorder.v15274logplain
-rw-r--r--Zpow_alt.v2561logplain
-rw-r--r--Zpow_def.v1332logplain
-rw-r--r--Zpow_facts.v8011logplain
-rw-r--r--Zpower.v9544logplain
-rw-r--r--Zquot.v14359logplain
-rw-r--r--Zsqrt_compat.v7703logplain
-rw-r--r--Zwf.v2518logplain
-rw-r--r--auxiliary.v2397logplain