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/coqargs.ml  | 8 +++-----
 sysinit/coqargs.mli | 1 +
 sysinit/coqinit.ml  | 1 +
 3 files changed, 5 insertions(+), 5 deletions(-)

(limited to 'sysinit')

diff --git a/sysinit/coqargs.ml b/sysinit/coqargs.ml
index ac9e430d31..faa26423e5 100644
--- a/sysinit/coqargs.ml
+++ b/sysinit/coqargs.ml
@@ -25,10 +25,6 @@ let error_missing_arg s =
 (* Imperative effects! This must be fixed at some point.                      *)
 (******************************************************************************)
 
-let set_type_in_type () =
-  let typing_flags = Environ.typing_flags (Global.env ()) in
-  Global.set_typing_flags { typing_flags with Declarations.check_universes = false }
-
 let set_debug () =
   let () = Exninfo.record_backtrace true in
   Flags.debug := true
@@ -52,6 +48,7 @@ type injection_command =
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
+  type_in_type      : bool;
   toplevel_name     : top;
 }
 
@@ -109,6 +106,7 @@ let default_native = Coq_config.native_compiler
 let default_logic_config = {
   impredicative_set = Declarations.PredicativeSet;
   indices_matter = false;
+  type_in_type = false;
   toplevel_name = TopLogical default_toplevel;
 }
 
@@ -435,7 +433,7 @@ let parse_args ~usage ~init arglist : t * string list =
       Flags.make_warn false;
       oval
     |"-time" -> { oval with config = { oval.config with time = true }}
-    |"-type-in-type" -> set_type_in_type (); oval
+    |"-type-in-type" -> set_logic (fun o -> { o with type_in_type = true }) oval
     |"-unicode" -> add_vo_require oval "Utf8_core" None (Some false)
     |"-where" -> set_query oval PrintWhere
     |"-h"|"-H"|"-?"|"-help"|"--help" -> set_query oval (PrintHelp usage)
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli
index acf941f730..cc622fabe3 100644
--- a/sysinit/coqargs.mli
+++ b/sysinit/coqargs.mli
@@ -33,6 +33,7 @@ type injection_command =
 type coqargs_logic_config = {
   impredicative_set : Declarations.set_predicativity;
   indices_matter    : bool;
+  type_in_type      : bool;
   toplevel_name     : top;
 }
 
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