From e5a2bcfff486137a25b28e4d574638ac52fd1d84 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 27 Mar 2020 12:25:41 +0100
Subject: [PATCH] sbi_internal_eq: add "sections" of notation, following stdpp

---
 tests/proofmode.v       | 4 ++++
 theories/bi/interface.v | 6 ++++++
 2 files changed, 10 insertions(+)

diff --git a/tests/proofmode.v b/tests/proofmode.v
index 1c51da064..f657edfe7 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -5,6 +5,10 @@ Section tests.
 Context {PROP : sbi}.
 Implicit Types P Q R : PROP.
 
+Lemma type_sbi_internal_eq_annot P :
+  P ≡@{PROP} P ∧ (≡@{PROP}) P P ∧ (P ≡.) P ∧ (.≡ P) P.
+Proof. done. Qed.
+
 Lemma test_eauto_emp_isplit_biwand P : emp ⊢ P ∗-∗ P.
 Proof. eauto 6. Qed.
 
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 1d0895ae6..41313692c 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -290,6 +290,12 @@ Notation "∃ x .. y , P" :=
 Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
 
 Infix "≡" := sbi_internal_eq : bi_scope.
+Infix "≡@{ A }" := (sbi_internal_eq (A := A)) (only parsing) : bi_scope.
+
+Notation "( X ≡.)" := (sbi_internal_eq X) (only parsing) : bi_scope.
+Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
+Notation "(≡@{ A } )" := (sbi_internal_eq (A := A)) (only parsing) : bi_scope.
+
 Notation "â–· P" := (sbi_later P) : bi_scope.
 
 Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
-- 
GitLab