From 2ac3d11f6f1332250e918ef628eca3b788b3550a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 16 Oct 2020 20:06:26 +0200
Subject: [environ] [typing_flags] Introduce helper function to remove
 duplicate code

---
 proofs/proof.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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
-- 
cgit v1.2.3