diff --git a/_CoqProject b/_CoqProject
index 1211cbed0529c738bdb43a0fe4613700e3149d70..364dba269a6104900e754ad8118c26c59dc2cb96 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -29,6 +29,7 @@ theories/bi/interface.v
 theories/bi/derived_connectives.v
 theories/bi/derived_laws.v
 theories/bi/big_op.v
+theories/bi/updates.v
 theories/bi/bi.v
 theories/bi/tactics.v
 theories/bi/fractional.v
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index 4f016b1ecab6ad26864fd87b90a25820dedcfc87..e2246a5c391cd3fc32d40ee4a062e1df734a45d1 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -1,5 +1,5 @@
 From iris.algebra Require Export cmra updates.
-From iris.bi Require Export derived_connectives.
+From iris.bi Require Export derived_connectives updates.
 From stdpp Require Import finite.
 Set Default Proof Using "Type".
 Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 8e90d845f18483d4895004e58ec0c4fe5652082d..c0846ea376d94809ddf816012f093cf3b804fcba 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -1,4 +1,4 @@
-From iris.bi Require Export derived_laws big_op.
+From iris.bi Require Export derived_laws big_op updates.
 Set Default Proof Using "Type".
 
 Module Import bi.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index c14f5d56d9af76c9cb5491ed77de6f9acb40b2bb..5636c79946a6ab93641e126feb327e03c1f39d57 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -1,4 +1,3 @@
-From stdpp Require Import coPset.
 From iris.algebra Require Export ofe.
 Set Primitive Projections.
 
@@ -525,34 +524,3 @@ Proof. eapply sbi_mixin_later_false_em, sbi_sbi_mixin. Qed.
 End sbi_laws.
 
 End bi.
-
-Class BUpd (A : Type) : Type := bupd : A → A.
-Instance : Params (@bupd) 2.
-
-Notation "|==> Q" := (bupd Q)
-  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
-Notation "P ==∗ Q" := (P ⊢ |==> Q)
-  (at level 99, Q at level 200, only parsing) : stdpp_scope.
-Notation "P ==∗ Q" := (P -∗ |==> Q)%I
-  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
-
-Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
-Instance: Params (@fupd) 4.
-
-Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-
-Notation "|={ E }=> Q" := (fupd E E Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }=>  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=∗  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
new file mode 100644
index 0000000000000000000000000000000000000000..12a4558b050214a1aee5af5328b6cffee80a98d3
--- /dev/null
+++ b/theories/bi/updates.v
@@ -0,0 +1,33 @@
+From stdpp Require Import coPset.
+From iris.bi Require Import interface.
+
+Class BUpd (A : Type) : Type := bupd : A → A.
+Instance : Params (@bupd) 2.
+
+Notation "|==> Q" := (bupd Q)
+  (at level 99, Q at level 200, format "|==>  Q") : bi_scope.
+Notation "P ==∗ Q" := (P ⊢ |==> Q)
+  (at level 99, Q at level 200, only parsing) : stdpp_scope.
+Notation "P ==∗ Q" := (P -∗ |==> Q)%I
+  (at level 99, Q at level 200, format "P  ==∗  Q") : bi_scope.
+
+Class FUpd (A : Type) : Type := fupd : coPset → coPset → A → A.
+Instance: Params (@fupd) 4.
+
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }=>  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
+  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
+
+Notation "|={ E }=> Q" := (fupd E E Q)
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }=>  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=∗  Q") : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
+  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.