diff options
| author | Pierre-Marie Pédrot | 2018-11-28 08:47:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-28 08:47:40 +0100 |
| commit | b106042cc1d752e69c0f3d218d794a79f27853cc (patch) | |
| tree | 60b77d18c9abd10d2439eb0b5ce7ab7a2d02796a /pretyping/classops.ml | |
| parent | 7db1dbb91439eecad777064fcbb8a8e904fc690d (diff) | |
| parent | df85d9b765940b58a189b91cfdc67be7e0fd75e3 (diff) | |
Merge PR #8727: [options] New helper for creation of boolean options plus reference.
Diffstat (limited to 'pretyping/classops.ml')
| -rw-r--r-- | pretyping/classops.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 1edcc499f0..f18040accb 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -398,16 +398,12 @@ let class_params = function let add_class cl = add_new_class cl { cl_param = class_params cl } -let automatically_import_coercions = ref false - -open Goptions -let () = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic import of coercions"; - optkey = ["Automatic";"Coercions";"Import"]; - optread = (fun () -> !automatically_import_coercions); - optwrite = (:=) automatically_import_coercions } +let get_automatically_import_coercions = + Goptions.declare_bool_option_and_ref + ~depr:true (* Remove in 8.8 *) + ~name:"automatic import of coercions" + ~key:["Automatic";"Coercions";"Import"] + ~value:false let cache_coercion (_, c) = let () = add_class c.coercion_source in @@ -425,7 +421,7 @@ let cache_coercion (_, c) = add_coercion_in_graph (xf,is,it) let load_coercion _ o = - if !automatically_import_coercions then + if get_automatically_import_coercions () then cache_coercion o let set_coercion_in_scope (_, c) = @@ -435,7 +431,7 @@ let set_coercion_in_scope (_, c) = let open_coercion i o = if Int.equal i 1 then begin set_coercion_in_scope o; - if not !automatically_import_coercions then + if not (get_automatically_import_coercions ()) then cache_coercion o end |