summaryrefslogtreecommitdiff
path: root/contrib/ring
ModeNameSize
-rw-r--r--LegacyArithRing.v2645logplain
-rw-r--r--LegacyNArithRing.v1485logplain
-rw-r--r--LegacyRing.v1432logplain
-rw-r--r--LegacyRing_theory.v10417logplain
-rw-r--r--LegacyZArithRing.v1369logplain
-rw-r--r--Quote.v2656logplain
-rw-r--r--Ring_abstract.v19905logplain
-rw-r--r--Ring_normalize.v26766logplain
-rw-r--r--Setoid_ring.v683logplain
-rw-r--r--Setoid_ring_normalize.v37411logplain
-rw-r--r--Setoid_ring_theory.v11025logplain
-rw-r--r--g_quote.ml4773logplain
-rw-r--r--g_ring.ml43855logplain
-rw-r--r--quote.ml16799logplain
-rw-r--r--ring.ml32755logplain