aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
ModeNameSize
-rw-r--r--Algebra_syntax.v1599logplain
-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.v1980logplain
-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.v4175logplain
-rw-r--r--Ring.v1604logplain
-rw-r--r--Ring_base.v967logplain
-rw-r--r--Ring_polynom.v43391logplain
-rw-r--r--Ring_tac.v15724logplain
-rw-r--r--Ring_theory.v19173logplain
-rw-r--r--Rings_Q.v1455logplain
-rw-r--r--Rings_R.v1595logplain
-rw-r--r--Rings_Z.v1004logplain
-rw-r--r--ZArithRing.v1692logplain
-rw-r--r--g_newring.ml45666logplain
-rw-r--r--newring.ml39987logplain
-rw-r--r--newring.mli1404logplain
-rw-r--r--newring_ast.ml2197logplain
-rw-r--r--newring_ast.mli2197logplain
-rw-r--r--newring_plugin.mlpack30logplain