From 0099a8f8e1a77a224ff133fc211d5a8b983a7dcc Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 4 Mar 2018 00:39:05 +0100 Subject: univ minimization: simplify try-with block around find_insts --- engine/universes.ml | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'engine') diff --git a/engine/universes.ml b/engine/universes.ml index fcde6b29c..727e50d6b 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -865,15 +865,16 @@ let minimize_univ_variables ctx us algs left right cstrs = instantiate_with_lbound u lbound lower ~alg:false ~enforce:false acc' else acc, {enforce=true; alg=false; lbound; lower} | None -> - try - (* Another universe represents the same lower bound, - we can share them with no harm. *) - let can, lower = find_inst insts lbound in - let lower = LMap.remove can lower in - instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc - with Not_found -> - (* We set u as the canonical universe representing lbound *) - instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc + begin match find_inst insts lbound with + | can, lower -> + (* Another universe represents the same lower bound, + we can share them with no harm. *) + let lower = LMap.remove can lower in + instantiate_with_lbound u (Universe.make can) lower ~alg:false ~enforce:false acc + | exception Not_found -> + (* We set u as the canonical universe representing lbound *) + instantiate_with_lbound u lbound lower ~alg:false ~enforce:true acc + end in let acc' acc = match LMap.find u right with -- cgit v1.2.3