diff --git a/tests/proofmode.v b/tests/proofmode.v
index 56d90ffdb86317384ffdd6f920fd51714599b04c..4443bbb9df7ce6788d3bdf8c5f75d0fd8785c12d 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -185,7 +185,7 @@ Lemma test_TC_resolution `{!BiAffine PROP} (Φ : nat → PROP) l x :
   x ∈ l → ([∗ list] y ∈ l, Φ y) -∗ Φ x.
 Proof.
   iIntros (Hp) "HT".
-  iDestruct (bi.big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
+  iDestruct (big_sepL_elem_of _ _ _ Hp with "HT") as "Hp".
   done.
 Qed.
 
diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index 86a7c24b8443ef2fb8f4a4b8194c9cd7f641cdd8..95fbe03a91bea11f7685a5698cd1ffe727f59ae3 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -6,16 +6,8 @@ Module Import bi.
   Export bi.interface.bi.
   Export bi.derived_laws_bi.bi.
   Export bi.derived_laws_sbi.bi.
-  (* For better compatibility with some developments created during
-     gen_proofmode times, also provide bigops inside the bi
-     module. *)
-  Export bi.big_op.bi.
 End bi.
 
-(* For better compatibility with pre-gen_proofmode-Iris, also provide
-   bigops outside of the bi module. *)
-Export bi.big_op.bi.
-
 (* Hint DB for the logic *)
 Hint Resolve pure_intro.
 Hint Resolve or_elim or_intro_l' or_intro_r' : BI.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 477105c84aa61c7e293ebb5250780fe555f0f606..277d29308e971469de904717ede6cfca051d6c69 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -2,6 +2,7 @@ From iris.algebra Require Export big_op.
 From iris.bi Require Import derived_laws_sbi plainly.
 From stdpp Require Import countable fin_collections functions.
 Set Default Proof Using "Type".
+Import interface.bi derived_laws_bi.bi.
 
 (* Notations *)
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l)
@@ -40,8 +41,6 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
    format "[∗  mset]  x  ∈  X ,  P") : bi_scope.
 
 (** * Properties *)
-Module bi.
-Import interface.bi derived_laws_bi.bi.
 Section bi_big_op.
 Context {PROP : bi}.
 Implicit Types Ps Qs : list PROP.
@@ -876,4 +875,3 @@ Section gmultiset.
   End plainly.
 End gmultiset.
 End sbi_big_op.
-End bi.
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index db8bce58ea5e4176d1ccdb663418150ecca69e3b..3874e71e4aa6ed5e1195b43a3bac1b84491e0a27 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -2096,13 +2096,13 @@ below; see the discussion in !75 for further details. *)
 Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
   rewrite envs_entails_eq; apply bi.internal_eq_refl.
 Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepL_nil'.
+  rewrite envs_entails_eq; apply big_sepL_nil'.
 Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepM_empty'.
+  rewrite envs_entails_eq; apply big_sepM_empty'.
 Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepS_empty'.
+  rewrite envs_entails_eq; apply big_sepS_empty'.
 Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
-  rewrite envs_entails_eq; apply bi.big_sepMS_empty'.
+  rewrite envs_entails_eq; apply big_sepMS_empty'.
 
 Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros.
 Hint Extern 0 (envs_entails _ (_ → _)) => iIntros.