From 3c8525f8c27791f437bb62a2402015faeff35ad7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Dec 2021 17:56:08 +0100
Subject: [PATCH] =?UTF-8?q?Add=20=E2=88=97-=E2=88=97=20as=20notation=20in?=
 =?UTF-8?q?=20stdpp=5Fscope=20similar=20to=20-=E2=88=97.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 iris/bi/derived_connectives.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index a5f5d62b3..fe6d60b1d 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -12,6 +12,7 @@ Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
 Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Global Instance: Params (@bi_wand_iff) 1 := {}.
 Infix "∗-∗" := bi_wand_iff : bi_scope.
+Notation "P ∗-∗ Q" := (⊢ P ∗-∗ Q) : stdpp_scope.
 
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Global Arguments Persistent {_} _%I : simpl never.
-- 
GitLab