diff --git a/iris/proofmode/notation.v b/iris/proofmode/notation.v
index e3dc8650e48f74e21fc8f968521488ae45c95031..fd847649903f6ffa7abb9d84c103e0b2e4057153 100644
--- a/iris/proofmode/notation.v
+++ b/iris/proofmode/notation.v
@@ -18,6 +18,7 @@ Notation "Γ '_' : P" := (Esnoc Γ (IAnon _) P%I)
 
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
   (envs_entails (Envs Γ Δ _) Q%I)
+  (* The level of Δ is picked to silence warnings about incompatible prefixes. See https://github.com/coq/coq/issues/19631. *)
   (at level 1, Δ at level 200, Q at level 200, left associativity,
   format "'[' Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q ']'", only printing) :
   stdpp_scope.