diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-03 23:47:54 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-13 14:10:04 +0200 |
| commit | e6b732d6fbb84d54eb3796e9fa1d10421532f3cd (patch) | |
| tree | 355848c41b76787ff0cfc16ad2da75569529e54f /engine | |
| parent | f53890d1629ea7aaff86ea92e5ac27ab027b2e8d (diff) | |
minimize_univ_variables: remove [and right] abbreviation.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/universes.ml | 9 |
1 files changed, 3 insertions, 6 deletions
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 |