[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.

1 files changed, 4 insertions, 18 deletions

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