summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring
ModeNameSize
-rw-r--r--ArithRing.v1781logplain
-rw-r--r--BinList.v2691logplain
-rw-r--r--Field.v581logplain
-rw-r--r--Field_tac.v14397logplain
-rw-r--r--Field_theory.v66335logplain
-rw-r--r--InitialRing.v17193logplain
-rw-r--r--NArithRing.v764logplain
-rw-r--r--RealField.v3436logplain
-rw-r--r--Ring.v1449logplain
-rw-r--r--Ring_base.v788logplain
-rw-r--r--Ring_equiv.v1635logplain
-rw-r--r--Ring_polynom.v54199logplain
-rw-r--r--Ring_tac.v11424logplain
-rw-r--r--Ring_theory.v19849logplain
-rw-r--r--ZArithRing.v1334logplain
-rw-r--r--newring.ml437667logplain