From e6b732d6fbb84d54eb3796e9fa1d10421532f3cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Sat, 3 Mar 2018 23:47:54 +0100
Subject: minimize_univ_variables: remove [and right] abbreviation.

---
 engine/universes.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/universes.ml b/engine/universes.ml
index d1caf40ac..ce1180764 100644
--- a/engine/universes.ml
+++ b/engine/universes.ml
@@ -842,9 +842,6 @@ let minimize_univ_variables ctx us algs left right cstrs =
         let left = List.uniquize (List.filter not_lower left) in
         (acc, left, LMap.union newlow lower)
       with Not_found -> acc, [], LMap.empty
-    and right =
-      try Some (LMap.find u right)
-      with Not_found -> None
     in
     let instantiate_lbound lbound =
       let alg = LSet.mem u algs in
@@ -878,9 +875,9 @@ let minimize_univ_variables ctx us algs left right cstrs =
 	    instantiate_with_lbound u lbound lower false true acc
     in
     let acc' acc = 
-      match right with
-      | None -> acc
-      | Some cstrs -> 
+      match LMap.find u right with
+      | exception Not_found -> acc
+      | cstrs ->
 	let dangling = List.filter (fun (d, r) -> not (LMap.mem r us)) cstrs in
 	  if List.is_empty dangling then acc
 	  else
-- 
cgit v1.2.3