aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/newring_plugin.mlpack
AgeCommit message (Expand)Author
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias
2016-06-08Compilation via pack for plugins of the stdlibPierre Letouzey