diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index ea78bca9c6d87d982c9bffb1a448f6cce6573144..7b153697c9c3807acd20393b38056589f881d008 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -16,7 +16,7 @@ Section bi_mixin.
   Context (bi_wand : PROP → PROP → PROP).
   Context (bi_persistently : PROP → PROP).
 
-  Local Bind Scope bi_scope with PROP.
+  Bind Scope bi_scope with PROP.
   Local Infix "⊢" := bi_entails.
   Local Notation "'emp'" := bi_emp : bi_scope.
   Local Notation "'True'" := (bi_pure True) : bi_scope.