aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
ModeNameSize
-rw-r--r--Algebra_syntax.v924logplain
-rw-r--r--ArithRing.v1783logplain
-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.v25223logplain
-rw-r--r--Integral_domain.v1304logplain
-rw-r--r--NArithRing.v769logplain
-rw-r--r--Ncring.v9480logplain
-rw-r--r--Ncring_initial.v6205logplain
-rw-r--r--Ncring_polynom.v16994logplain
-rw-r--r--Ncring_tac.v9439logplain
-rw-r--r--RealField.v3499logplain
-rw-r--r--Ring.v1454logplain
-rw-r--r--Ring_base.v817logplain
-rw-r--r--Ring_polynom.v43061logplain
-rw-r--r--Ring_tac.v15047logplain
-rw-r--r--Ring_theory.v18407logplain
-rw-r--r--Rings_Q.v779logplain
-rw-r--r--Rings_R.v919logplain
-rw-r--r--Rings_Z.v328logplain
-rw-r--r--ZArithRing.v1542logplain
-rw-r--r--g_newring.ml45397logplain
-rw-r--r--newring.ml39573logplain
-rw-r--r--newring.mli1276logplain
-rw-r--r--newring_ast.mli2030logplain
-rw-r--r--newring_plugin.mlpack18logplain