aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
ModeNameSize
-rw-r--r--Algebra_syntax.v924logplain
-rw-r--r--ArithRing.v2133logplain
-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.v54339logplain
-rw-r--r--InitialRing.v26724logplain
-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.v43241logplain
-rw-r--r--Ring_tac.v15048logplain
-rw-r--r--Ring_theory.v19019logplain
-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.ml45565logplain
-rw-r--r--newring.ml39770logplain
-rw-r--r--newring.mli1276logplain
-rw-r--r--newring_ast.mli2032logplain
-rw-r--r--newring_plugin.mlpack18logplain