From c7aee488d7aa16a40e707590e055ac9d9afc5382 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Thu, 3 Oct 2024 08:23:18 +0000
Subject: [PATCH] Add comment

---
 iris/proofmode/notation.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/iris/proofmode/notation.v b/iris/proofmode/notation.v
index e3dc8650e..fd8476499 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.
-- 
GitLab