aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
ModeNameSize
-rw-r--r--Algebra_syntax.v924logplain
-rw-r--r--ArithRing.v2283logplain
-rw-r--r--BinList.v2358logplain
-rw-r--r--Cring.v9132logplain
-rw-r--r--Field.v731logplain
-rw-r--r--Field_tac.v19722logplain
-rw-r--r--Field_theory.v54489logplain
-rw-r--r--InitialRing.v26874logplain
-rw-r--r--Integral_domain.v1304logplain
-rw-r--r--NArithRing.v919logplain
-rw-r--r--Ncring.v9630logplain
-rw-r--r--Ncring_initial.v6355logplain
-rw-r--r--Ncring_polynom.v17144logplain
-rw-r--r--Ncring_tac.v9589logplain
-rw-r--r--RealField.v3499logplain
-rw-r--r--Ring.v1604logplain
-rw-r--r--Ring_base.v967logplain
-rw-r--r--Ring_polynom.v43391logplain
-rw-r--r--Ring_tac.v15048logplain
-rw-r--r--Ring_theory.v19173logplain
-rw-r--r--Rings_Q.v779logplain
-rw-r--r--Rings_R.v919logplain
-rw-r--r--Rings_Z.v328logplain
-rw-r--r--ZArithRing.v1692logplain
-rw-r--r--g_newring.ml45672logplain
-rw-r--r--newring.ml39921logplain
-rw-r--r--newring.mli1426logplain
-rw-r--r--newring_ast.ml2200logplain
-rw-r--r--newring_ast.mli2200logplain
-rw-r--r--newring_plugin.mlpack30logplain