aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrfwd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssr/ssrfwd.ml')
-rw-r--r--plugins/ssr/ssrfwd.ml10
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