[environ] [typing_flags] Introduce helper function to remove duplicate code

6 files changed, 10 insertions, 10 deletions

diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 3f2f0f8755..c54adb45f9 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -113,7 +113,7 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt =
 let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = false in
   let env = Global.env() in
-  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+  let env = Environ.update_typing_flags ?typing_flags env in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, types), impargs =
@@ -134,7 +134,7 @@ let do_definition ?hook ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl r
 let do_definition_program ?hook ~pm ~name ~scope ~poly ?typing_flags ~kind ?using udecl bl red_option c ctypopt =
   let program_mode = true in
   let env = Global.env() in
-  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+  let env = Environ.update_typing_flags ?typing_flags env in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = interp_univ_decl_opt env udecl in
   let evd, (body, types), impargs =
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1184cd96ac..0cf0b07822 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -245,7 +245,7 @@ let interp_fixpoint ?(check_recursivity=true) ?typing_flags ~cofix l :
     UState.universe_decl * UState.t *
     (EConstr.rel_context * Impargs.manual_implicits * int option) list) =
   let env = Global.env () in
-  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+  let env = Environ.update_typing_flags ?typing_flags env in
   let (env,_,pl,evd),fix,info = interp_recursive env ~program_mode:false ~cofix l in
   if check_recursivity then check_recursive true env evd fix;
   let evd = Pretyping.(solve_remaining_evars all_no_fail_flags env evd) in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5c859e2f01..2be6097184 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -641,7 +641,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ?typing_flags ~pr
       | NonUniformParameters -> ([], params, indl)
   in
   let env = Global.env () in
-  let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+  let env = Environ.update_typing_flags ?typing_flags env in
   let mie,pl,impls = interp_mutual_inductive_gen env ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (DeclareInd.declare_mutual_inductive_with_eliminations ?typing_flags mie pl impls);
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 9033df1673..3c4a651cf5 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -284,7 +284,7 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl =
   let cofix = fixkind = Declare.Obls.IsCoFixpoint in
   let (env, rec_sign, udecl, evd), fix, info =
     let env = Global.env () in
-    let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+    let env = Environ.update_typing_flags ?typing_flags env in
     interp_recursive env ~cofix ~program_mode:true fixl
   in
     (* Program-specific code *)
@@ -323,9 +323,9 @@ let do_program_recursive ~pm ~scope ~poly ?typing_flags ?using fixkind fixl =
       in
       let indexes =
         let env = Global.env () in
-        let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+        let env = Environ.update_typing_flags ?typing_flags env in
         Pretyping.search_guard env possible_indexes fixdecls in
-      let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+      let env = Environ.update_typing_flags ?typing_flags env in
       List.iteri (fun i _ ->
           Inductive.check_fix env
             ((indexes,i),fixdecls))
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 74ace04a7c..fafee13bf6 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -588,7 +588,7 @@ let mutual_make_bodies ~typing_flags ~fixitems ~rec_declaration ~possible_indexe
   match possible_indexes with
   | Some possible_indexes ->
     let env = Global.env() in
-    let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+    let env = Environ.update_typing_flags ?typing_flags env in
     let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
     let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
     let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
@@ -1918,7 +1918,7 @@ end = struct
       (* Try all combinations... not optimal *)
       let env = Global.env() in
       let typing_flags = pinfo.Proof_info.info.Info.typing_flags in
-      let env = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env) env typing_flags in
+      let env = Environ.update_typing_flags ?typing_flags env in
       Internal.map_entry_body entry
         ~f:(guess_decreasing env possible_indexes)
     in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0801d8d83f..a3726daf63 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -550,7 +550,7 @@ let post_check_evd ~udecl ~poly evd =
 
 let start_lemma_com ~typing_flags ~program_mode ~poly ~scope ~kind ?using ?hook thms =
   let env0 = Global.env () in
-  let env0 = Option.cata (fun typing_flags -> Environ.set_typing_flags typing_flags env0) env0 typing_flags in
+  let env0 = Environ.update_typing_flags ?typing_flags env0 in
   let flags = Pretyping.{ all_no_fail_flags with program_mode } in
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrintern.interp_univ_decl_opt env0 (snd decl) in