diff options
| author | Hugo Herbelin | 2018-10-29 11:27:15 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-31 16:16:41 +0100 |
| commit | d1091555104e0198eaaa94a1bb69e96d5cc73447 (patch) | |
| tree | dd5f0704a368604e27944c48b1a735c9ab4a8369 /vernac | |
| parent | ae39925d64cc51663ab3f2ad397501b435bd0e5e (diff) | |
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..4df50a5e23 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 = (fun b -> Global.set_typing_flags { (Global.typing_flags ()) with Declarations.share_reduction = b }) } let _ = declare_bool_option |