6 files changed, 47 insertions, 0 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9a75f0b682..1b17e954b7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -418,6 +418,7 @@ let set_engagement c env = (* Unsafe *)
 (* It's convenient to use [{flags with foo = bar}] so we're smart wrt to it. *)
 let same_flags {
      check_guarded;
+     check_positive;
      check_universes;
      conv_oracle;
      indices_matter;
@@ -426,6 +427,7 @@ let same_flags {
      enable_native_compiler;
   } alt =
   check_guarded == alt.check_guarded &&
+  check_positive == alt.check_positive &&
   check_universes == alt.check_universes &&
   conv_oracle == alt.conv_oracle &&
   indices_matter == alt.indices_matter &&
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ea45f699ce..6970a11e72 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -194,6 +194,18 @@ let set_typing_flags c senv =
   if env == senv.env then senv
   else { senv with env }
 
+let set_check_guarded b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_guarded = b } senv
+
+let set_check_positive b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_positive = b } senv
+
+let set_check_universes b senv =
+  let flags = Environ.typing_flags senv.env in
+  set_typing_flags { flags with check_universes = b } senv
+
 let set_indices_matter indices_matter senv =
   set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2406b6add1..fa53fa33fa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -130,6 +130,9 @@ val set_engagement : Declarations.engagement -> safe_transformer0
 val set_indices_matter : bool -> safe_transformer0
 val set_typing_flags : Declarations.typing_flags -> safe_transformer0
 val set_share_reduction : bool -> safe_transformer0
+val set_check_guarded : bool -> safe_transformer0
+val set_check_positive : bool -> safe_transformer0
+val set_check_universes : bool -> safe_transformer0
 val set_VM : bool -> safe_transformer0
 val set_native_compiler : bool -> safe_transformer0
 val make_sprop_cumulative : safe_transformer0
diff --git a/library/global.ml b/library/global.ml
index ca774dbd74..0fc9e11364 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -89,6 +89,9 @@ let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
 let set_engagement c = globalize0 (Safe_typing.set_engagement c)
 let set_indices_matter b = globalize0 (Safe_typing.set_indices_matter b)
 let set_typing_flags c = globalize0 (Safe_typing.set_typing_flags c)
+let set_check_guarded c = globalize0 (Safe_typing.set_check_guarded c)
+let set_check_positive c = globalize0 (Safe_typing.set_check_positive c)
+let set_check_universes c = globalize0 (Safe_typing.set_check_universes c)
 let typing_flags () = Environ.typing_flags (env ())
 let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
diff --git a/library/global.mli b/library/global.mli
index d034bc4208..b089b7dd80 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -31,6 +31,9 @@ val named_context : unit -> Constr.named_context
 val set_engagement : Declarations.engagement -> unit
 val set_indices_matter : bool -> unit
 val set_typing_flags : Declarations.typing_flags -> unit
+val set_check_guarded : bool -> unit
+val set_check_positive : bool -> unit
+val set_check_universes : bool -> unit
 val typing_flags : unit -> Declarations.typing_flags
 val make_sprop_cumulative : unit -> unit
 val set_allow_sprop : bool -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4fb0129236..f90439d222 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1724,6 +1724,30 @@ let () =
       optread  = Nativenorm.get_profiling_enabled;
       optwrite = Nativenorm.set_profiling_enabled }
 
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "guard checking";
+      optkey   = ["Guard"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_guarded);
+      optwrite = (fun b -> Global.set_check_guarded b) }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "positivity/productivity checking";
+      optkey   = ["Positivity"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_positive);
+      optwrite = (fun b -> Global.set_check_positive b) }
+
+let _ =
+  declare_bool_option
+    { optdepr  = false;
+      optname  = "universes checking";
+      optkey   = ["Universes"; "Checking"];
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.check_universes);
+      optwrite = (fun b -> Global.set_check_universes b) }
+
 let vernac_set_strategy ~local l =
   let local = Option.default false local in
   let glob_ref r =