diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0b8006eeeccd..3098a7c3db4f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -557,7 +557,7 @@ Enabling and disabling notations Cannot enable or disable for parsing a notation that was originally defined as only printing. - .. exn:: Found no matching notation to enable or disable. + .. warn:: Found no matching notation to enable or disable. No previously defined notation satisfies the given constraints. diff --git a/interp/notation.ml b/interp/notation.ml index 33a5725119d0..a8c231024a48 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -2671,6 +2671,11 @@ let toggle_abbreviations ~on found ntn_pattern = Abbreviation.toggle_abbreviations ~on ~use:ntn_pattern.use_pattern test with Exit -> () +let warn_nothing_to_enable_or_disable = + CWarnings.create ~name:"no-notation-to-enable-or-disable" + ~category:CWarnings.CoreCategories.syntax + (fun () -> strbrk "Found no matching notation to enable or disable.") + let toggle_notations ~on ~all ?(verbose=true) prglob ntn_pattern = let found = ref [] in (* Deal with (parsing) notations *) @@ -2688,8 +2693,7 @@ let toggle_notations ~on ~all ?(verbose=true) prglob ntn_pattern = (* Deal with abbreviations *) toggle_abbreviations ~on found ntn_pattern; match !found with - | [] -> - user_err (strbrk "Found no matching notation to enable or disable.") + | [] -> warn_nothing_to_enable_or_disable () | _::_::_ when not all -> user_err (strbrk "More than one interpretation bound to this notation, confirm with the \"all\" modifier.") | _ -> diff --git a/test-suite/output/activation.out b/test-suite/output/activation.out index 3d64de5d38c7..81997a456483 100644 --- a/test-suite/output/activation.out +++ b/test-suite/output/activation.out @@ -5,12 +5,13 @@ modifier. File "./output/activation.v", line 12, characters 0-22: The command has indeed failed with message: No notation provided. -File "./output/activation.v", line 15, characters 0-24: +File "./output/activation.v", line 16, characters 0-24: The command has indeed failed with message: Found no matching notation to enable or disable. +[no-notation-to-enable-or-disable,syntax,default] a : Type -File "./output/activation.v", line 24, characters 11-12: +File "./output/activation.v", line 26, characters 11-12: The command has indeed failed with message: The reference a was not found in the current environment. Prop @@ -25,6 +26,7 @@ x : bool 0 : nat -File "./output/activation.v", line 44, characters 0-49: +File "./output/activation.v", line 47, characters 0-49: The command has indeed failed with message: Found no matching notation to enable or disable. +[no-notation-to-enable-or-disable,syntax,default] diff --git a/test-suite/output/activation.v b/test-suite/output/activation.v index 6b6f16c8e7ca..3513c23a6de5 100644 --- a/test-suite/output/activation.v +++ b/test-suite/output/activation.v @@ -12,7 +12,9 @@ Disable Notation (all) : nat_scope. Fail Disable Notation. Module Abbrev. +Set Warnings "+no-notation-to-enable-or-disable". Fail Disable Notation f. (* no abbreviation with such suffix *) +Set Warnings "no-notation-to-enable-or-disable". Notation f w := (S w). Disable Notation f w := (S w). Enable Notation := (S _). @@ -41,6 +43,8 @@ End Abbrev. Module Bug17782. Declare Custom Entry trm. +Set Warnings "+no-notation-to-enable-or-disable". Fail Disable Notation "'foo' _" (in custom trm). +Set Warnings "no-notation-to-enable-or-disable". End Bug17782.