From 0a531fae53c31ef76ff25fbfd3ceb8b5b33aa264 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 6 Jan 2021 17:31:33 +0100
Subject: [coqargs] use standard option injection for -type-in-type

---
 sysinit/coqinit.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'sysinit/coqinit.ml')

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);
-- 
cgit v1.2.3