diff options
author | 2018-07-02 12:56:50 +0200 | |
---|---|---|
committer | 2018-07-02 12:56:50 +0200 | |
commit | f6f606232ae3c32e5c90d4fd427721875529b777 (patch) | |
tree | 078e8778e2bc6da1b5b7ca2e641a931e8d08ddfe /plugins/setoid_ring/newring_ast.ml | |
parent | 033c32a32fedcf2160bb38a3fed55efa9d1c2b77 (diff) | |
parent | f8190123ff989e38f9e196260119453b13739ded (diff) |
Merge PR #7961: [api] Fix wrong deprecation warning (#7915)
Diffstat (limited to 'plugins/setoid_ring/newring_ast.ml')
0 files changed, 0 insertions, 0 deletions