diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |