aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
ModeNameSize
-rw-r--r--Algebra_syntax.v924logplain
-rw-r--r--ArithRing.v1779logplain
-rw-r--r--BinList.v2208logplain
-rw-r--r--Cring.v8982logplain
-rw-r--r--Field.v581logplain
-rw-r--r--Field_tac.v19572logplain
-rw-r--r--Field_theory.v53831logplain
-rw-r--r--InitialRing.v25192logplain
-rw-r--r--Integral_domain.v1304logplain
-rw-r--r--NArithRing.v767logplain
-rw-r--r--Ncring.v9480logplain
-rw-r--r--Ncring_initial.v6171logplain
-rw-r--r--Ncring_polynom.v16994logplain
-rw-r--r--Ncring_tac.v9439logplain
-rw-r--r--RealField.v3239logplain
-rw-r--r--Ring.v1448logplain
-rw-r--r--Ring_base.v817logplain
-rw-r--r--Ring_polynom.v43066logplain
-rw-r--r--Ring_tac.v14545logplain
-rw-r--r--Ring_theory.v18420logplain
-rw-r--r--Rings_Q.v779logplain
-rw-r--r--Rings_R.v919logplain
-rw-r--r--Rings_Z.v328logplain
-rw-r--r--ZArithRing.v1534logplain
-rw-r--r--newring.ml442510logplain
-rw-r--r--newring_plugin.mllib27logplain
-rw-r--r--vo.itarget320logplain