Backport PR coq#18734: Changelog for coq#18670

SkySkimmer · Feb 29, 2024 · 7676ad0 · 7676ad0
2 parents 2d640cd + d25e26a
commit 7676ad0
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 0 deletions.
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
@@ -654,6 +654,14 @@ Kernel
   (`#18599 <https://github.com/coq/coq/pull/18599>`_,
   by Guillaume Melquiond).
 
+Notations
+^^^^^^^^^
+
+- **Changed:**
+  :warn:`Found no matching notation to enable or disable` is a warning instead of an error
+  (`#18670 <https://github.com/coq/coq/pull/18670>`_,
+  by Pierre Roux).
+
 Tactics
 ^^^^^^^
 

diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -558,6 +558,7 @@ Enabling and disabling notations
       originally defined as only printing.
 
    .. warn:: Found no matching notation to enable or disable.
+      :name: Found no matching notation to enable or disable
 
       No previously defined notation satisfies the given constraints.