Merge pull request #20 from SkySkimmer/push-context-strict

Adapt to coq/coq#19620 (Global.push_context_set no strict argument)
SkySkimmer · Oct 14, 2024 · c513cee · c513cee
2 parents 810eee3 + 666376d
commit c513cee
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/lean.ml b/src/lean.ml
@@ -457,7 +457,7 @@ let rec level_of_sets uconv n =
         if lean_fancy_univs () then level_of_universe_core [ (Level.set, n) ]
         else UnivGen.fresh_level ()
       in
-      Global.push_context_set ~strict:true
+      Global.push_context_set
         (Level.Set.singleton l, Constraints.singleton (p, Lt, l));
       sets := Int.Map.add n l !sets;
       let graph = add_universe l ~lbound:p uconv.graph in