diff options
| author | Pierre-Marie Pédrot | 2015-04-15 09:52:13 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-04-15 09:52:13 +0200 |
| commit | 148cf78a4d85ec56818a8ff00719a775670950b9 (patch) | |
| tree | ea4540bb896b3bbedb7c41b80fcf7e0ff1cd04aa /library | |
| parent | 429f493997e34bfaac930c68bf6b267a5b9640ee (diff) | |
| parent | 6f40831dc1d0fecfbaf9fbc8116da0e74b6e8726 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'library')
| -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 |