diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-04 00:26:30 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-13 14:10:04 +0200 |
| commit | 5e4690453afb7898d2760f18201740517ae99d70 (patch) | |
| tree | 335e36c3055d19fd90c602421666b38c4af5d3b1 /engine | |
| parent | 9384726b851097957a139907907ced72f1ae461b (diff) | |
univ minimization: s/[failwith ""]/[raise UpperBoundedAlg]/
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/universes.ml | 7 |
1 files changed, 5 insertions, 2 deletions
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 |