diff --git a/interp/notation.ml b/interp/notation.ml index 7160bd0478e10..ad17dc27b312b 100644 --- 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 index 638ed1f1c0446..ebf0e1aa6bac0 100644 --- 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 index fe12845a6efba..6b6f16c8e7ca5 100644 --- 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.