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.

1 files changed, 3 insertions, 0 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