aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/declare.ml2
-rw-r--r--library/universes.ml4
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