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;