summaryrefslogtreecommitdiff
path: root/contrib/ring
ModeNameSize
-rw-r--r--LegacyArithRing.v2645logplain
-rw-r--r--LegacyNArithRing.v1485logplain
-rw-r--r--LegacyRing.v1439logplain
-rw-r--r--LegacyRing_theory.v10421logplain
-rw-r--r--LegacyZArithRing.v1369logplain
-rw-r--r--Quote.v2656logplain
-rw-r--r--Ring_abstract.v19908logplain
-rw-r--r--Ring_normalize.v26770logplain
-rw-r--r--Setoid_ring.v683logplain
-rw-r--r--Setoid_ring_normalize.v37412logplain
-rw-r--r--Setoid_ring_theory.v11029logplain
-rw-r--r--g_quote.ml4773logplain
-rw-r--r--g_ring.ml43855logplain
-rw-r--r--quote.ml16863logplain
-rw-r--r--ring.ml32819logplain