From d1091555104e0198eaaa94a1bb69e96d5cc73447 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 29 Oct 2018 11:27:15 +0100
Subject: Seeing Global purely as a wrapper on top of kernel functions.

---
 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 1190d73258..4df50a5e23 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_reduction_sharing b) }
+      optwrite = (fun b -> Global.set_typing_flags { (Global.typing_flags ()) with Declarations.share_reduction = b }) }
 
 let _ =
   declare_bool_option
-- 
cgit v1.2.3