aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.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 /pretyping/typeclasses_errors.ml
parent5e4690453afb7898d2760f18201740517ae99d70 (diff)
univ minimization: simplify try-with block around find_insts
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions