diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 2 | ||||
| -rw-r--r-- | library/universes.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index 5968fbf38b..994a6557ad 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -431,7 +431,7 @@ let cache_universes (p, l) = Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l in - Global.push_context_set false ctx; + Global.push_context_set p ctx; if p then Lib.add_section_context ctx; Universes.set_global_universe_names glob' diff --git a/library/universes.ml b/library/universes.ml index 1b6f7a9d57..a8e9478e13 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -820,7 +820,7 @@ let minimize_univ_variables ctx us algs left right cstrs = let cstrs' = List.fold_left (fun cstrs (d, r) -> if d == Univ.Le then enforce_leq inst (Universe.make r) cstrs - else + else try let lev = Option.get (Universe.level inst) in Constraint.add (lev, d, r) cstrs with Option.IsNone -> failwith "") |