From 2b00d1e68d1c84528a500bb24d4f06d3d91f829b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 8 Jun 2014 22:46:34 +0200
Subject: Adding a toplevel option allowing to deactivate the term sharing in
 kernel reduction.

---
 toplevel/vernacentries.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8e424a96ff..65326774f9 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1241,6 +1241,15 @@ let _ =
 	           let lev = Option.default Flags.default_inline_level o in
 	           Flags.set_inline_level lev) }
 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "kernel term sharing";
+      optkey   = ["Kernel"; "Term"; "Sharing"];
+      optread  = (fun () -> !Closure.share);
+      optwrite = (fun b -> Closure.share := b) }
+
 let _ =
   declare_bool_option
     { optsync  = true;
-- 
cgit v1.2.3