diff options
| author | Gaëtan Gilbert | 2018-03-04 00:56:30 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-04-13 14:10:04 +0200 |
| commit | 8e00ec838eadffb5c868fdbfa693471cdd80ef8c (patch) | |
| tree | d5eeb736b1c1e97ac653690710ffd92d4b7b0cd4 /plugins/syntax/string_syntax.ml | |
| parent | c097b83dc9a33a2410e61b8d2aa667229fbd411c (diff) | |
univ minimization: use shadowing more
This avoids having multiple highly similar things in scope when we
only want one of them.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions