From d25e26a4f11db643eea004f03ba1287fc3e0b766 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 29 Feb 2024 14:57:38 +0100 Subject: [PATCH] Changelog for #18670 (cherry picked from commit 01d0d0c4f8d25ae94f364a4678b808ff55d53326) --- doc/sphinx/changes.rst | 8 ++++++++ doc/sphinx/user-extensions/syntax-extensions.rst | 1 + 2 files changed, 9 insertions(+) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5e016a33c727..56154aeb85a8 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -654,6 +654,14 @@ Kernel (`#18599 `_, by Guillaume Melquiond). +Notations +^^^^^^^^^ + +- **Changed:** + :warn:`Found no matching notation to enable or disable` is a warning instead of an error + (`#18670 `_, + by Pierre Roux). + Tactics ^^^^^^^ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index a0f32abf6e1d..86f078d7f52e 100644 --- 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.