From c3ea3cd8a2bd29fc0129e34af4a1689bbf7519a5 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 31 Oct 2018 16:09:43 +0100
Subject: Introduce Safe_typing.set_share_reduction

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4df50a5e23..5eace14cbf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1536,7 +1536,7 @@ let _ =
       optname  = "kernel term sharing";
       optkey   = ["Kernel"; "Term"; "Sharing"];
       optread  = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
-      optwrite = (fun b -> Global.set_typing_flags { (Global.typing_flags ()) with Declarations.share_reduction = b }) }
+      optwrite = Global.set_share_reduction }
 
 let _ =
   declare_bool_option
-- 
cgit v1.2.3