Merge PR coq#19935: Bypass warning override when possible

Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Dec 16, 2024 · 9e82aef · 9e82aef
2 parents 0508d64 + 47a4ad9
commit 9e82aef
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/vernac/declare.ml b/vernac/declare.ml
@@ -978,8 +978,9 @@ let declare_possibly_mutual_definitions ~info ~cinfo ~obls ?(is_telescope=false)
   let () =
     (* For the recursive case, we override the temporary notations used while proving, now using the global names *)
     let local = info.scope=Locality.Discharge in
-    CWarnings.with_warn ("-"^Notation.warning_overridden_name)
-      (List.iter (Metasyntax.add_notation_interpretation ~local (Global.env()))) ntns
+    if ntns <> [] then
+      CWarnings.with_warn ("-"^Notation.warning_overridden_name)
+        (List.iter (Metasyntax.add_notation_interpretation ~local (Global.env()))) ntns
   in
   refs