diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index a5f5d62b307d37a701303d1f47e8b93bf65c7a0b..fe6d60b1d37ad8a69986ddde71d8525979aafd05 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.