aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
ModeNameSize
-rw-r--r--dune171logplain
-rw-r--r--g_newring.mlg4952logplain
-rw-r--r--newring.ml37746logplain
-rw-r--r--newring.mli1293logplain
-rw-r--r--newring_ast.ml2258logplain
-rw-r--r--newring_ast.mli2258logplain
-rw-r--r--newring_plugin.mlpack30logplain