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.
---
 kernel/cClosure.mli | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'kernel/cClosure.mli')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index 1e3e7b48ac..6121b3a1ec 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -15,7 +15,6 @@ open Esubst
 
 (** Flags for profiling reductions. *)
 val stats : bool ref
-val share : bool ref
 
 val with_stats: 'a Lazy.t -> 'a
 
@@ -106,8 +105,13 @@ type 'a infos = {
   i_cache : 'a infos_cache }
 
 val ref_value_cache: 'a infos -> 'a infos_tab -> table_key -> 'a option
-val create: ('a infos -> 'a infos_tab -> constr -> 'a) -> reds -> env ->
-  (existential -> constr option) -> 'a infos
+val create:
+  repr:('a infos -> 'a infos_tab -> constr -> 'a) ->
+  share:bool ->
+  reds ->
+  env ->
+  (existential -> constr option) ->
+  'a infos
 val create_tab : unit -> 'a infos_tab
 val evar_value : 'a infos_cache -> existential -> constr option
 
-- 
cgit v1.2.3