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