Fixing coq#17782: Not_found to catch on non-existing custom notation …

…to disable.
herbelin · Jul 26, 2023 · ead0777 · ead0777
1 parent 4d3970f
commit ead0777
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 5 deletions.
diff --git a/interp/notation.ml b/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 ->

diff --git a/test-suite/output/activation.out b/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.
diff --git a/test-suite/output/activation.v b/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.