diff options
| author | Maxime Dénès | 2018-09-03 12:36:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-03 12:36:45 +0200 |
| commit | 3bc0c82700a805e889198b810cc0148f6479cbe1 (patch) | |
| tree | eac2cce0546a79cb5786e0570c0c55b9b4438e4b /vernac | |
| parent | 7456164386a87df83763109e12fa8aaa71a96104 (diff) | |
| parent | 14a1786158ec093faa172a5b95a93b06ad43b7af (diff) | |
Merge PR #7085: Turn the kernel reduction sharing flag into an argument passed in the cache
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 5258ab2ea4..e1c9712135 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1505,8 +1505,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 |