Fixes #17782: anomaly when trying to disable a non existing custom notation

doc/changelog/03-notations/17891-master+fix17782-anomaly-disable-non-existing-custom-notation.rst

@@ -0,0 +1,5 @@
+- **Fixed:**
+  Anomaly when trying to disable a non-existent custom notation
+  (`#17891 <https://github.com/coq/coq/pull/17891>`_,
+  fixes `#17782 <https://github.com/coq/coq/issues/17782>`_,
+  by Hugo Herbelin).

interp/notation.ml

@@ -2497,11 +2497,14 @@ let toggle_notations_in_scope ~on found inscope ntn_pattern ntns =
   | _ :: _ as ntn_entries, Some (Inl ntn) ->
     (* shortcut *)
     List.fold_right (fun ntn_entry ntns ->
-      NotationMap.add (ntn_entry, ntn)
-        (toggle_notations_by_interpretation ~on found ntn_pattern
-           (inscope,(ntn_entry,ntn))
-           (NotationMap.find (ntn_entry, ntn) ntns))
-        ntns) ntn_entries ntns
+      try
+        NotationMap.add (ntn_entry, ntn)
+          (toggle_notations_by_interpretation ~on found ntn_pattern
+             (inscope,(ntn_entry,ntn))
+             (NotationMap.find (ntn_entry, ntn) ntns))
+          ntns
+      with Not_found -> ntns)
+        ntn_entries ntns
     (* Deal with full notations *)
   | ntn_entries, ntn_rule -> (* This is the table of notations, not of abbreviations *)
     NotationMap.mapi (fun (ntn_entry,ntn_key' as ntn') data ->

test-suite/output/activation.out

@@ -68,3 +68,6 @@ The following notations have been enabled:
 Notation activation.Abbrev.x := 0
 0
      : nat
+File "./output/activation.v", line 44, characters 0-49:
+The command has indeed failed with message:
+Found no matching notation to enable or disable.

test-suite/output/activation.v

@@ -37,3 +37,10 @@ Enable Notation x.
 Check x.
 
 End Abbrev.
+
+Module Bug17782.
+
+Declare Custom Entry trm.
+Fail Disable Notation "'foo' _"  (in custom trm).
+
+End Bug17782.