Remove declare_object for SsrHave NoTCResolution.

IIUC, this was a hack to make `Set SsrHave NoTCResolution` behave like
`Global Set SsrHave NoTCResolution`. I don't think it is needed (just
let the user write the desired locality), but if it is, the right way of
doing it is to let clients of Goptions specify a default locality.

2 files changed, 5 insertions, 8 deletions

diff --git a/CHANGES b/CHANGES
index 2df231f26..d3f07889f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,9 @@ Vernacular Commands
   overwritting the opacity set of the hint database.
 - Added generic syntax for “attributes”, as in:
   `#[local] Lemma foo : bar.`
+- The `Set SsrHave NoTCResolution` command no longer has special global
+  scope. If you want the previous behavior, use `Global Set SsrHave
+  NoTCResolution`.
 
 Coq binaries and process model
 
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