diff options
Diffstat (limited to 'sysinit/coqinit.ml')
| -rw-r--r-- | sysinit/coqinit.ml | 1 |
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); |