summaryrefslogtreecommitdiff
path: root/contrib/setoid_ring
ModeNameSize
-rw-r--r--ArithRing.v1918logplain
-rw-r--r--BinList.v2683logplain
-rw-r--r--Field.v581logplain
-rw-r--r--Field_tac.v7326logplain
-rw-r--r--Field_theory.v48067logplain
-rw-r--r--InitialRing.v16210logplain
-rw-r--r--NArithRing.v965logplain
-rw-r--r--RealField.v2664logplain
-rw-r--r--Ring.v1429logplain
-rw-r--r--Ring_base.v788logplain
-rw-r--r--Ring_equiv.v1635logplain
-rw-r--r--Ring_polynom.v39277logplain
-rw-r--r--Ring_tac.v5147logplain
-rw-r--r--Ring_theory.v17086logplain
-rw-r--r--ZArithRing.v1012logplain
-rw-r--r--newring.ml433279logplain