diff options
| author | Emilio Jesus Gallego Arias | 2018-04-24 18:46:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-04-26 12:58:15 +0200 |
| commit | 81545ec98255e644be589d34a521924549e9e2fa (patch) | |
| tree | 65ab59d21e680a00e379deffa440f038b5d0c121 /plugins/syntax/string_syntax.ml | |
| parent | 0f107c8a747af6bdb40d70d80236f84b325dc35d (diff) | |
[api] Move `hint_info_expr` to `Typeclasses`.
`hint_info_expr`, `hint_info_gen` do conceptually belong to the
typeclasses modules and should be able to be used without a dependency
on the concrete vernacular syntax.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions