From 50802fbc22c96706189a070ab7e9da6f34a90409 Mon Sep 17 00:00:00 2001
From: Yann Leray <yann.leray@inria.fr>
Date: Thu, 5 Feb 2026 14:48:44 +0100
Subject: [PATCH] Adapt to rocq-prover/rocq#21531 (stricter type-in-type)

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

diff --git a/src/lean.ml b/src/lean.ml
index 985f9ac..85a31bd 100644
--- a/src/lean.ml
+++ b/src/lean.ml
@@ -219,7 +219,7 @@ let lean_scheme env ~dep mind u s =
 
 let with_unsafe_univs f () =
   let flags = Global.typing_flags () in
-  Global.set_typing_flags { flags with check_universes = false };
+  Global.set_typing_flags { flags with check_eliminations = false };
   try
     let v = f () in
     Global.set_typing_flags flags;