diff options
| author | Gaëtan Gilbert | 2017-12-05 13:39:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-02-14 15:39:28 +0100 |
| commit | 20916bd558a355b597337101e3281bb5ebbfcd36 (patch) | |
| tree | 06946e7bb2f8928872ae4e18c945e7c3443dca8d /plugins/syntax/string_syntax.ml | |
| parent | d2fb531761e1f4fa02d0c7e7b5b51febe48e357e (diff) | |
detype_case predicate is not optional
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions