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

9 files changed, 17 insertions, 11 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 69edb1498c..a5f81d1e59 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -479,6 +479,9 @@ let set_typing_flags c env =
     let env = set_type_in_type (not c.check_universes) env in
     env
 
+let update_typing_flags ?typing_flags env =
+  Option.cata (fun flags -> set_typing_flags flags env) env typing_flags
+
 let set_cumulative_sprop b env =
   set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 6a8ddce835..900e2128ea 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -351,6 +351,9 @@ val set_type_in_type : bool -> env -> env
 val set_allow_sprop : bool -> env -> env
 val sprop_allowed : env -> bool
 
+(** [update_typing_flags ?typing_flags] may update env with optional typing flags *)
+val update_typing_flags : ?typing_flags:typing_flags -> env -> env
+
 val universes_of_global : env -> GlobRef.t -> AUContext.t
 
 (** {6 Sets of referred section variables }
diff --git a/proofs/proof.ml b/proofs/proof.ml
index e9c8ce6746..50a0e63700 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -563,7 +563,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
-    let env = Option.cata (fun f -> Environ.set_typing_flags f env) env pr.typing_flags in
+    let env = Environ.update_typing_flags ?typing_flags:pr.typing_flags env in
     let (p,(status,info),()) = run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
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