diff options
| author | Gaëtan Gilbert | 2019-12-30 13:03:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-07 10:15:45 +0100 |
| commit | 1220aab80893b68c14adb64ba0b75811961ac04d (patch) | |
| tree | a9eecd12c75e8b33cc5b0d9d9d4a3369e67c9d48 /plugins/syntax/string_notation.mli | |
| parent | a7de863bf68f6aae3832e8c8d5b000576d107a63 (diff) | |
minor cleanup template_polymorphic_univs: check_levels returns bool
Diffstat (limited to 'plugins/syntax/string_notation.mli')
0 files changed, 0 insertions, 0 deletions