From 666376d435e1e0d8c0e177fdc04270b871da987c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Tue, 1 Oct 2024 15:59:04 +0200
Subject: [PATCH] Adapt to coq/coq#19620 (Global.push_context_set no strict
 argument)

---
 src/lean.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/lean.ml b/src/lean.ml
index 4d04668..dd5af85 100644
--- 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