diff options
| author | Gaëtan Gilbert | 2017-11-21 16:42:42 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-14 19:17:49 +0100 |
| commit | 30746e6a9a3296c1aacb2fc03e1c16014232219f (patch) | |
| tree | f3390677c41221e01cce72543f74c8984e6eec6a /plugins/syntax/string_syntax.ml | |
| parent | f9b715c4ea07d6ecfece7f28e4d25f3dcab01158 (diff) | |
Deprecate dead code option Congruence Depth.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions