From de20a45db5d45154819f2ed4359effdbb8bf0292 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 27 Mar 2018 16:16:40 +0200
Subject: Turn the kernel reduction sharing flag into an argument passed in the
 cache.

We move the global declaration of that argument to the environment, and reuse
the Global module to handle this flag.

Note that the checker was not using this flag before this patch, and still
doesn't use it. This should probably be fixed in a later patch.
---
 vernac/vernacentries.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 653f8b26e0..d33c278e31 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1501,8 +1501,8 @@ let _ =
     { optdepr  = false;
       optname  = "kernel term sharing";
       optkey   = ["Kernel"; "Term"; "Sharing"];
-      optread  = (fun () -> !CClosure.share);
-      optwrite = (fun b -> CClosure.share := b) }
+      optread  = (fun () -> (Global.typing_flags ()).Declarations.share_reduction);
+      optwrite = (fun b -> Global.set_reduction_sharing b) }
 
 let _ =
   declare_bool_option
-- 
cgit v1.2.3