From 5e4690453afb7898d2760f18201740517ae99d70 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sun, 4 Mar 2018 00:26:30 +0100 Subject: univ minimization: s/[failwith ""]/[raise UpperBoundedAlg]/ --- engine/universes.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'engine') diff --git a/engine/universes.ml b/engine/universes.ml index 6b2c76036..fcde6b29c 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -789,6 +789,8 @@ let _pr_constraints_map (cmap:constraints_map) = let remove_alg l (ctx, us, algs, insts, cstrs) = (ctx, us, LSet.remove l algs, insts, cstrs) +exception UpperBoundedAlg + let minimize_univ_variables ctx us algs left right cstrs = let left, lbounds = Univ.LMap.fold (fun r lower (left, lbounds as acc) -> @@ -887,7 +889,7 @@ let minimize_univ_variables ctx us algs left right cstrs = else try let lev = Option.get (Universe.level inst) in Constraint.add (lev, d, r) cstrs - with Option.IsNone -> failwith "") + with Option.IsNone -> raise UpperBoundedAlg) cstrs dangling in (ctx', us, algs, insts, cstrs'), b @@ -900,7 +902,8 @@ let minimize_univ_variables ctx us algs left right cstrs = acc' (acc, {enforce=true;alg=false;lbound=Universe.make u; lower}) | Some lbound -> try acc' (instantiate_lbound lbound) - with Failure _ -> acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) + with UpperBoundedAlg -> + acc' (acc, {enforce=true; alg=false; lbound=Universe.make u; lower}) and aux (ctx', us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u -- cgit v1.2.3