From d308a3ad11f38ce3d504a3d29f9894affdd1fbcc Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 18 Jul 2018 09:17:20 +0200 Subject: 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. --- CHANGES | 3 +++ plugins/ssr/ssrfwd.ml | 10 ++-------- 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 -- cgit v1.2.3