diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 10:56:08 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2018-07-20 10:56:08 +0200 |
commit | 2de309b65b379a3c496752aa25f1cfc177644222 (patch) | |
tree | 2808a0a0a7ce02805488c3d936567ea30d90eaa0 /plugins | |
parent | 161910e3cd7726751ca545262ef8f9c7a69b2a3c (diff) | |
parent | d308a3ad11f38ce3d504a3d29f9894affdd1fbcc (diff) |
Merge PR #8089: Remove declare_object for SsrHave NoTCResolution.
Diffstat (limited to 'plugins')
-rw-r--r-- | plugins/ssr/ssrfwd.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 7fe2421f9..e367cd32d 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -68,20 +68,14 @@ open Ssripats let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false -let inHaveTCResolution = Libobject.declare_object { - (Libobject.default_object "SSRHAVETCRESOLUTION") with - Libobject.cache_function = (fun (_,v) -> ssrhaveNOtcresolution := v); - Libobject.load_function = (fun _ (_,v) -> ssrhaveNOtcresolution := v); - Libobject.classify_function = (fun v -> Libobject.Keep v); -} let _ = Goptions.declare_bool_option { Goptions.optname = "have type classes"; Goptions.optkey = ["SsrHave";"NoTCResolution"]; Goptions.optread = (fun _ -> !ssrhaveNOtcresolution); Goptions.optdepr = false; - Goptions.optwrite = (fun b -> - Lib.add_anonymous_leaf (inHaveTCResolution b)) } + Goptions.optwrite = (fun b -> ssrhaveNOtcresolution := b); + } open Constrexpr |