diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-05 18:12:55 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-05 18:12:55 +0200 |
| commit | e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 (patch) | |
| tree | db7cefecb217083cf3284c122ee4ce4c4a4eb56a /plugins/setoid_ring/newring.ml | |
| parent | cd76a274c7d6fb71e109b6f3c87dd3a661f72e6c (diff) | |
Remove dead code and unused open.
Diffstat (limited to 'plugins/setoid_ring/newring.ml')
0 files changed, 0 insertions, 0 deletions