diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-04 14:48:24 +0200 |
commit | af19d08003173718c0f7c070d0021ad958fbe58d (patch) | |
tree | e148de88bbc70d6cd1561dffba2f301181bbb2f5 /plugins/ssr/ssrelim.mli | |
parent | 90ac335a32afc6bbca5c11b7be7aabc1f7abb89b (diff) | |
parent | 81545ec98255e644be589d34a521924549e9e2fa (diff) |
Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.
Diffstat (limited to 'plugins/ssr/ssrelim.mli')
0 files changed, 0 insertions, 0 deletions