[coqargs] use standard option injection for -type-in-type

1 files changed, 1 insertions, 0 deletions

diff --git a/sysinit/coqinit.ml b/sysinit/coqinit.ml
index cbecc52827..16c8389de5 100644
--- a/sysinit/coqinit.ml
+++ b/sysinit/coqinit.ml
@@ -105,6 +105,7 @@ let init_runtime opts =
   (* Configuration *)
   Global.set_engagement opts.config.logic.impredicative_set;
   Global.set_indices_matter opts.config.logic.indices_matter;
+  Global.set_check_universes (not opts.config.logic.type_in_type);
   Global.set_VM opts.config.enable_VM;
   Flags.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);
   Global.set_native_compiler (match opts.config.native_compiler with NativeOff -> false | NativeOn _ -> true);