diff --git a/theories/bi/bi.v b/theories/bi/bi.v
index b1d4c8a7826b010556fbd4783ca6a587c0b4ea1d..86a7c24b8443ef2fb8f4a4b8194c9cd7f641cdd8 100644
--- a/theories/bi/bi.v
+++ b/theories/bi/bi.v
@@ -6,9 +6,16 @@ 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/program_logic/lifting.v b/theories/program_logic/lifting.v
index 8ddf09130437c36c936d6973154e5fa9b2131604..64f74293b1983ce859686e279d6409857a1de740 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -104,7 +104,7 @@ Proof.
   iApply (wp_lift_pure_det_step with "[HWP]").
   - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
   - destruct s; naive_solver.
-  - by rewrite bi.big_sepL_nil right_id.
+  - by rewrite big_sepL_nil right_id.
 Qed.
 
 Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index f31ade3336b8ca858acee445b15e122bb506ec14..2601d7ae71d009637dacf187136199780c868ee2 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -170,7 +170,7 @@ Section lifting.
     {{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
   Proof.
     intros. rewrite -(ownP_lift_atomic_det_step σ1 v2 σ2 []); [|done..].
-    rewrite bi.big_sepL_nil right_id. by apply bi.wand_intro_r.
+    rewrite big_sepL_nil right_id. by apply bi.wand_intro_r.
   Qed.
 
   Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
@@ -188,7 +188,7 @@ Section lifting.
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
-    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?bi.big_sepL_nil ?right_id; eauto.
+    intros. rewrite -(wp_lift_pure_det_step e1 e2 []) ?big_sepL_nil ?right_id; eauto.
   Qed.
 End lifting.