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.

1 files changed, 1 insertions, 0 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index bbe4bc0dcb..b0d8410873 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -21,6 +21,7 @@ let safe_flags oracle = {
   check_guarded = true;
   check_universes = true;
   conv_oracle = oracle;
+  share_reduction = true;
 }
 
 (** {6 Arities } *)