From 82b8ee7dc168d5007359755d009c47939085fc31 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Apr 2022 23:22:04 +0200
Subject: [PATCH] Comments.

---
 iris/base_logic/upred.v | 2 ++
 iris/si_logic/siprop.v  | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index d2b54213a..6df52f94e 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -435,6 +435,8 @@ Implicit Types A : Type.
 Local Arguments uPred_holds {_} !_ _ _ /.
 Local Hint Immediate uPred_in_entails : core.
 
+(** The notations below are implicitly local due to the section, so we do not
+mind the overlap with the general BI notations. *)
 Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
 Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
 Notation "P ⊣⊢ Q" := (@uPred_equiv M P%I Q%I) : stdpp_scope.
diff --git a/iris/si_logic/siprop.v b/iris/si_logic/siprop.v
index dc7fef0a5..fa9af40b4 100644
--- a/iris/si_logic/siprop.v
+++ b/iris/si_logic/siprop.v
@@ -128,6 +128,8 @@ Ltac unseal := rewrite !unseal_eqs /=.
 Section primitive.
 Local Arguments siProp_holds !_ _ /.
 
+(** The notations below are implicitly local due to the section, so we do not
+mind the overlap with the general BI notations. *)
 Notation "P ⊢ Q" := (siProp_entails P Q).
 Notation "'True'" := (siProp_pure True) : bi_scope.
 Notation "'False'" := (siProp_pure False) : bi_scope.
-- 
GitLab