aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_syntax.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-03-04 00:39:05 +0100
committerGaëtan Gilbert2018-04-13 14:10:04 +0200
commit0099a8f8e1a77a224ff133fc211d5a8b983a7dcc (patch)
tree363b998fafa40a3221cc7a653516ac8539e688a6 /plugins/syntax/string_syntax.ml
parent5e4690453afb7898d2760f18201740517ae99d70 (diff)
univ minimization: simplify try-with block around find_insts
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions