diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 2 | ||||
| -rw-r--r-- | library/universes.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index 5968fbf38..994a6557a 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 a157a747c..96937b3b3 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -815,7 +815,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 "") @@ -849,7 +849,7 @@ let normalize_context_set ctx us algs = Constraint.fold (fun (l,d,r as cstr) (smallles, noneqs) -> if d == Le then if Univ.Level.is_small l then - if is_set_minimization () then + if is_set_minimization () && LSet.mem r ctx then (Constraint.add cstr smallles, noneqs) else (smallles, noneqs) else if Level.is_small r then |