From 9384726b851097957a139907907ced72f1ae461b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 4 Mar 2018 00:13:18 +0100 Subject: univ minimization: simplify try-with block around [find u left] This makes it clear where the Not_found can come from. --- engine/universes.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'engine') diff --git a/engine/universes.ml b/engine/universes.ml index ca6ce7184..6b2c76036 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -804,8 +804,9 @@ let minimize_univ_variables ctx us algs left right cstrs = in let rec instance (ctx', us, algs, insts, cstrs as acc) u = let acc, left, lower = - try - let l = LMap.find u left in + match LMap.find u left with + | exception Not_found -> acc, [], LMap.empty + | l -> let acc, left, newlow, lower = List.fold_left (fun (acc, left', newlow, lower') (d, l) -> @@ -840,7 +841,6 @@ let minimize_univ_variables ctx us algs left right cstrs = in let left = List.uniquize (List.filter not_lower left) in (acc, left, LMap.union newlow lower) - with Not_found -> acc, [], LMap.empty in let instantiate_lbound lbound = let alg = LSet.mem u algs in -- cgit v1.2.3