diff options
| author | Matthieu Sozeau | 2015-04-09 17:10:27 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-04-09 17:10:27 +0200 |
| commit | b322c6131ab45be2d65ab2f6fcbcde7588314260 (patch) | |
| tree | 94af60bca9751415bdb29e12d17e4f4913dac0d8 | |
| parent | fd19fbb3720f1f1d930dcd082ddcd021cb6e8b50 (diff) | |
Strengthen minimization: it shouldn't set a universe u to a max if it
has a strict upper bound.
| -rw-r--r-- | library/universes.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/library/universes.ml b/library/universes.ml index 51c2b4d851..9fddc7067b 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -772,7 +772,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 -> assert false) + with Option.IsNone -> failwith "") cstrs dangling in (ctx', us, algs, insts, cstrs'), b @@ -784,7 +784,8 @@ let minimize_univ_variables ctx us algs left right cstrs = | None -> (* Nothing to do *) acc' (acc, (true, false, Universe.make u)) | Some lbound -> - acc' (instantiate_lbound lbound) + try acc' (instantiate_lbound lbound) + with Failure _ -> acc' (acc, (true, false, Universe.make u)) and aux (ctx', us, algs, seen, cstrs as acc) u = try acc, LMap.find u seen with Not_found -> instance acc u |