[kernel] Allow to set typing flags in add_constant

This is just an experiment, but makes the uses of the API easier as we
don't mess with the global state anymore.

5 files changed, 19 insertions, 19 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 6abd283f6c..1ecb5cba7d 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -247,6 +247,15 @@ let set_native_compiler b senv =
 
 let set_allow_sprop b senv = { senv with env = Environ.set_allow_sprop b senv.env }
 
+(* Temporary sets custom typing flags *)
+let with_typing_flags ?typing_flags senv ~f =
+  match typing_flags with
+  | None -> f senv
+  | Some typing_flags ->
+    let orig_typing_flags = Environ.typing_flags senv.env in
+    let res, senv = f (set_typing_flags typing_flags senv) in
+    res, set_typing_flags orig_typing_flags senv
+
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
 let check_engagement env expected_impredicative_set =
@@ -928,6 +937,9 @@ let add_constant l decl senv =
   in
   kn, senv
 
+let add_constant ?typing_flags l decl senv =
+  with_typing_flags ?typing_flags senv ~f:(add_constant l decl)
+
 let add_private_constant l decl senv : (Constant.t * private_constants) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
     let cb =
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 6fa9022906..c4d0fffe2b 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -93,6 +93,7 @@ val export_private_constants :
 
 (** returns the main constant *)
 val add_constant :
+  ?typing_flags:Declarations.typing_flags ->
   Label.t -> global_declaration -> Constant.t safe_transformer
 
 (** Similar to add_constant but also returns a certificate *)
diff --git a/library/global.ml b/library/global.ml
index 5c847fda96..238b9d554b 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -105,7 +105,7 @@ let is_cumulative_sprop () = (typing_flags()).Declarations.cumulative_sprop
 let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b)
 let sprop_allowed () = Environ.sprop_allowed (env())
 let export_private_constants cd = globalize (Safe_typing.export_private_constants cd)
-let add_constant id d = globalize (Safe_typing.add_constant (i2l id) d)
+let add_constant ?typing_flags id d = globalize (Safe_typing.add_constant ?typing_flags (i2l id) d)
 let add_private_constant id d = globalize (Safe_typing.add_private_constant (i2l id) d)
 let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie)
 let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl)
diff --git a/library/global.mli b/library/global.mli
index 5faf0e8bbd..4c2d427925 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -52,6 +52,7 @@ val export_private_constants :
   Safe_typing.exported_private_constant list
 
 val add_constant :
+  ?typing_flags:Declarations.typing_flags ->
   Id.t -> Safe_typing.global_declaration -> Constant.t
 val add_private_constant :
   Id.t -> Safe_typing.side_effect_declaration -> Constant.t * Safe_typing.private_constants
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 0b3b3aeb43..210007d17d 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -327,26 +327,10 @@ let cast_opaque_proof_entry (type a b) (entry : (a, b) effect_entry) (e : a proo
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 
 let is_unsafe_typing_flags flags =
+  let flags = Option.default (Global.typing_flags ()) flags in
   let open Declarations in
   not (flags.check_universes && flags.check_guarded && flags.check_positive)
 
-(* Maybe it would make sense to push this logic down to
-   Safe_typing.add_constant? *)
-let add_constant_with_flags ~typing_flags ~unsafe ~name decl =
-  let current_flags = Global.typing_flags () in
-  let typing_flags = Option.cata
-      (fun new_flags -> Global.set_typing_flags new_flags; new_flags)
-      current_flags typing_flags in
-  try
-    let kn = Global.add_constant name decl in
-    Global.set_typing_flags current_flags;
-    if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
-    kn
-  with exn ->
-    let ie = Exninfo.capture exn in
-    Global.set_typing_flags current_flags;
-    Exninfo.iraise ie
-
 let define_constant ~name ~typing_flags cd =
   (* Logically define the constant and its subproofs, no libobject tampering *)
   let decl, unsafe = match cd with
@@ -371,7 +355,9 @@ let define_constant ~name ~typing_flags cd =
     | PrimitiveEntry e ->
       ConstantEntry (Entries.PrimitiveEntry e), false
   in
-  add_constant_with_flags ~unsafe ~typing_flags ~name decl
+  let kn = Global.add_constant ?typing_flags name decl in
+  if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom();
+  kn
 
 let declare_constant ?(local = Locality.ImportDefaultBehavior) ~name ~kind ~typing_flags cd =
   let () = check_exists name in