univ minimization: simplify try-with block around find_insts

1 files changed, 10 insertions, 9 deletions

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