diff options
| author | Maxime Dénès | 2018-11-05 10:28:44 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-11-05 10:28:44 +0100 |
| commit | eb842684456c5a965507c83e7b169ae0d0f6cc90 (patch) | |
| tree | 3e7a55ef60b50af0bab3b4f5db99be35b488a068 /vernac | |
| parent | d813a48dcc80ca9763fd48d9e369bd21062c21d8 (diff) | |
| parent | c367e7cd962089d2932b986e5764b8e3844ad4b0 (diff) | |
Merge PR #8842: Towards seeing Global purely as a wrapper on top of kernel functions
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1190d73258..5eace14cbf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1536,7 +1536,7 @@ let _ = optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); - optwrite = (fun b -> Global.set_reduction_sharing b) } + optwrite = Global.set_share_reduction } let _ = declare_bool_option |