From 7a076b9bf33fcd7cef5789642ae62a8918a1a249 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 29 May 2018 14:59:29 +0200
Subject: [PATCH] big_ops moved out of the bi module

---
 theories/adequacy.v             |  4 ++--
 theories/base/ghosts.v          |  8 ++++----
 theories/bigop.v                |  4 ++--
 theories/blocks_generic.v       |  4 ++--
 theories/examples/circ_buffer.v |  8 ++++----
 theories/examples/list_lemmas.v |  6 +++---
 theories/examples/msqueue.v     |  4 ++--
 theories/examples/ticket_lock.v |  8 ++++----
 theories/gps/cas.v              | 14 +++++++-------
 theories/gps/fai.v              | 10 +++++-----
 theories/gps/init.v             |  6 +++---
 theories/gps/read.v             | 10 +++++-----
 theories/gps/write.v            | 18 +++++++++---------
 theories/iris_lemmas.v          |  4 ++--
 theories/malloc.v               |  4 ++--
 15 files changed, 56 insertions(+), 56 deletions(-)

diff --git a/theories/adequacy.v b/theories/adequacy.v
index 722d5c69..a5ef9c8f 100644
--- a/theories/adequacy.v
+++ b/theories/adequacy.v
@@ -220,10 +220,10 @@ Proof.
     iDestruct (own_big_op (to_hist σ) (λ k t, ◯ {[ k:= t]}) with "HH'") as "A".
     iDestruct (own_big_op (to_info σ) (λ k t, ◯ {[ k:= t]}) with "HI'") as "B".
     iCombine "A" "B" as "AB".
-    rewrite (bi.big_sepM_fmap _ _ (to_hist σ)). rewrite -bi.big_sepM_sepM.
+    rewrite (big_sepM_fmap _ _ (to_hist σ)). rewrite -big_sepM_sepM.
     match goal with
     | |- coq_tactics.envs_entails _ (big_opM _ ?f ?g) =>
-      iApply (bi.big_sepM_impl _ f with "[$AB]")
+      iApply (big_sepM_impl _ f with "[$AB]")
     end.
     iIntros "!#". iIntros (? ? ?) "[A B]". destruct a0.
     + iIntros (? ?). iFrame. iExists _. iFrame.
diff --git a/theories/base/ghosts.v b/theories/base/ghosts.v
index 47ce0670..0433fe29 100644
--- a/theories/base/ghosts.v
+++ b/theories/base/ghosts.v
@@ -565,8 +565,8 @@ Section UpdateGhosts.
     assert (HDel: delete l (<[l:=Excl h']> HIST) = delete l HIST).
       { symmetry. apply (partial_alter_compose (λ _, None) _ HIST). }
     rewrite /DInv.
-    rewrite (bi.big_sepM_delete _ (HIST) l (Excl h)); last assumption.
-    rewrite (bi.big_sepM_delete _ (<[l:=Excl h']> HIST) l (Excl h'));
+    rewrite (big_sepM_delete _ (HIST) l (Excl h)); last assumption.
+    rewrite (big_sepM_delete _ (<[l:=Excl h']> HIST) l (Excl h'));
        last by rewrite (lookup_insert HIST l (Excl h')).
     rewrite HDel.
     iIntros "[_ $]".
@@ -581,8 +581,8 @@ Section UpdateGhosts.
     assert (HDel: delete l (<[l:=Excl h']> HIST) = delete l HIST).
       { symmetry. apply (partial_alter_compose (λ _, None) _ HIST). }
     rewrite /DInv.
-    rewrite (bi.big_sepM_delete _ HIST l (Excl h)); last assumption.
-    rewrite (bi.big_sepM_delete _ (<[l:=Excl h']> HIST) l (Excl h'));
+    rewrite (big_sepM_delete _ HIST l (Excl h)); last assumption.
+    rewrite (big_sepM_delete _ (<[l:=Excl h']> HIST) l (Excl h'));
                 last by rewrite lookup_insert.
     rewrite HDel.
     iIntros "[HInfo [HHist [_ $]]]".
diff --git a/theories/bigop.v b/theories/bigop.v
index dbe5f7fd..ba58a651 100644
--- a/theories/bigop.v
+++ b/theories/bigop.v
@@ -11,11 +11,11 @@ Proof.
   induction j; first omega.
   rewrite /= -fmap_seq.
   destruct j as [|j].
-  - by rewrite bi.big_sepL_nil Pos2Qp_1 Qp_mult_1_l bi.sep_emp.
+  - by rewrite big_sepL_nil Pos2Qp_1 Qp_mult_1_l bi.sep_emp.
   - rewrite Nat2Pos.inj_succ; last omega.
     rewrite Pos2Qp_succ Qp_mult_plus_distr_l Qp_mult_1_l.
     rewrite fractional bi.sep_comm.
-    rewrite bi.big_sepL_fmap IHj; [auto|omega].
+    rewrite big_sepL_fmap IHj; [auto|omega].
 Qed.
 
 (* Section BigOp. *)
diff --git a/theories/blocks_generic.v b/theories/blocks_generic.v
index e04ef5b8..d199dc5e 100644
--- a/theories/blocks_generic.v
+++ b/theories/blocks_generic.v
@@ -76,12 +76,12 @@ Section Blocks.
     : Ψ a ∗ ([∗ set] b ∈ block_ends S, Ψ b)
       ⊢ ([∗ set] b ∈ block_ends ({[a]} ∪ S), Ψ b).
   Proof.
-    rewrite -bi.big_sepS_insert; last first.
+    rewrite -big_sepS_insert; last first.
     - move => In.
       apply (elem_of_subseteq (block_ends S) S) in In => //.
       by apply subseteq_gset_filter.
     - iIntros "H".
-      iApply (bi.big_sepS_subseteq (A:=A) with "H"). inversion B.
+      iApply (big_sepS_subseteq (A:=A) with "H"). inversion B.
       + rewrite BE. apply union_subseteq_r.
       + rewrite BE.
         apply union_mono_l, gset_difference_subseteq.
diff --git a/theories/examples/circ_buffer.v b/theories/examples/circ_buffer.v
index 19649986..ae0751d3 100644
--- a/theories/examples/circ_buffer.v
+++ b/theories/examples/circ_buffer.v
@@ -165,8 +165,8 @@ Section CircBuffer.
       ={↑escrowN}=∗ ([∗ list] i ∈ seq 0 ni, PE γ q i)%I.
     Proof.
       move => Le. iIntros "OL". iApply fupd_big_sepL.
-      rewrite (Nat2Z.id 2) -2!fmap_seq -list_fmap_compose bi.big_sepL_fmap.
-      iApply (bi.big_sepL_mono with "OL").
+      rewrite (Nat2Z.id 2) -2!fmap_seq -list_fmap_compose big_sepL_fmap.
+      iApply (big_sepL_mono with "OL").
       iIntros (? i H) "ol".
       apply lookup_seq_inv in H as [H1 H2]. simpl in H1. subst k.
       rewrite (_: Z.of_nat ((S ∘ S) i) = b + i `mod` n)%Z.
@@ -227,7 +227,7 @@ Section CircBuffer.
       rewrite (_ : Z.to_nat (n + b) = S $ S $ Z.to_nat n); last first.
         { rewrite Z2Nat.inj_add; [|omega|omega].
           rewrite (_: Z.to_nat 2 = 2%nat); last auto. omega. }
-      rewrite 2!bi.big_sepL_cons -/seq.
+      rewrite 2!big_sepL_cons -/seq.
       iDestruct "oLs" as "(owi & ori & oLs)".
 
       iAssert (|={⊤}=> ([∗ list] i ∈ seq 0 (Z.to_nat n), PE γ q i)%I)%I
@@ -244,7 +244,7 @@ Section CircBuffer.
         iSplitL ""; [auto|iNext]. iSplitL ""; iIntros "!#".
         - by rewrite Zmod_0_l.
         - simpl. iIntros (j). iIntros "%".
-          iDestruct (bi.big_sepL_lookup with "PEs") as "$".
+          iDestruct (big_sepL_lookup with "PEs") as "$".
           rewrite lookup_seq; [done|]. apply Nat2Z.inj_lt. lia'. }
 
       iNext. iIntros "cW".
diff --git a/theories/examples/list_lemmas.v b/theories/examples/list_lemmas.v
index ec63bf57..ea09b7d2 100644
--- a/theories/examples/list_lemmas.v
+++ b/theories/examples/list_lemmas.v
@@ -18,7 +18,7 @@ Lemma big_sepL_seq {A} (P : nat -> PROP) (l : list A):
   ([∗ list] i↦_ ∈ l, P i) ⊣⊢ ([∗ list] i ∈ seq 0 (length l), P i).
 Proof.
   induction l using rev_ind; first done.
-  rewrite app_length /= Nat.add_1_r seq_S !bi.big_sepL_app /=.
+  rewrite app_length /= Nat.add_1_r seq_S !big_sepL_app /=.
   by rewrite IHl Nat.add_0_r.
 Qed.
 
@@ -26,7 +26,7 @@ Lemma big_sepL_nth {A} (P : nat -> A -> PROP) l d:
   ([∗ list] i↦x ∈ l, P i x) ⊣⊢ ([∗ list] i ∈ seq 0 (length l), P i (nth i l d)).
 Proof.
   rewrite -big_sepL_seq.
-  apply bi.big_sepL_proper; intros.
+  apply big_sepL_proper; intros.
   erewrite nth_lookup_Some; eauto.
 Qed.
 
@@ -40,7 +40,7 @@ Lemma big_sepL_replicate {A} (P : nat -> A -> PROP) x n:
   ([∗ list] i↦x ∈ replicate n x, P i x) ⊣⊢ ([∗ list] i ∈ seq 0 n, P i x).
 Proof.
   rewrite big_sepL_nth replicate_length.
-  apply bi.big_sepL_proper; intros.
+  apply big_sepL_proper; intros.
   by erewrite nth_replicate.
 Qed.    
 
diff --git a/theories/examples/msqueue.v b/theories/examples/msqueue.v
index 460184cb..397fe829 100644
--- a/theories/examples/msqueue.v
+++ b/theories/examples/msqueue.v
@@ -190,7 +190,7 @@ Section MSQueue.
       iApply (wp_mask_mono); first auto.
       iApply (malloc_spec with "kI"); [omega|done|].
       iNext. iIntros (q) "oLs".
-      rewrite bi.big_sepL_cons /=.
+      rewrite big_sepL_cons /=.
       iDestruct "oLs" as "(oH & [oT _])". (* TODO: avoid emp *)
 
       wp_let. wp_bind ([_]_na <- _)%E. wp_op. wp_op.
@@ -285,7 +285,7 @@ Section MSQueue.
       iApply (wp_mask_mono); first auto.
       iApply (malloc_spec with "kI"); [omega|done|].
       iNext. iIntros (n) "oLs".
-      rewrite bi.big_sepL_cons /=.
+      rewrite big_sepL_cons /=.
       iDestruct "oLs" as "(ol & (od & _))". (* TODO: avoid emp *)
       wp_let. wp_bind ([_]_na <- _)%E. wp_op.
       iApply (na_write with "[$kI $od]"); [done|].
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 94917a58..82edca11 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -419,8 +419,8 @@ Section TicketLock.
        ⊢ ([∗ set] i ∈ seq_set j n, MyTkt γ i t)%I.
     Proof.
       revert j. induction n => j /=; iIntros "MyTkts".
-      - by rewrite bi.big_sepS_empty.
-      - rewrite bi.big_sepS_insert; last first.
+      - by rewrite big_sepS_empty.
+      - rewrite big_sepS_insert; last first.
         { move => /elem_of_seq_set [Le _]. omega. }
         rewrite /map_excl to_gmap_union_singleton insert_singleton_op;
           last first.
@@ -531,7 +531,7 @@ Section TicketLock.
       iApply (malloc_spec with "kI []"); [omega|done|].
 
       iNext. iIntros (x) "oLs".
-      rewrite bi.big_sepL_cons big_opL_singleton.
+      rewrite big_sepL_cons big_opL_singleton.
       iDestruct "oLs" as "(oNS & oTC)".
 
       wp_seq. wp_bind ([_]_na <- _)%E. wp_op.
@@ -582,7 +582,7 @@ Section TicketLock.
 
       iApply ("Post"  with "[MyTkts]").
 
-      iApply (bi.big_sepS_impl _ _ setC with "[$MyTkts]").
+      iApply (big_sepS_impl _ _ setC with "[$MyTkts]").
       iIntros "!#". iIntros (i) "_ Tkt".
       iExists γ, i, None. iFrame "Tkt TCP".
       iIntros "!#". by iIntros (?) "%".
diff --git a/theories/gps/cas.v b/theories/gps/cas.v
index e59d5caa..0d4db733 100644
--- a/theories/gps/cas.v
+++ b/theories/gps/cas.v
@@ -100,7 +100,7 @@ Section CAS.
               + rewrite -H2 elem_of_map_gset. by exists e'.
               + exists t. by rewrite -Eq -Eq1. }
 
-        rewrite /BE_Inv (bi.big_sepS_delete _ _ _ Heb).
+        rewrite /BE_Inv (big_sepS_delete _ _ _ Heb).
         iDestruct "oBEI" as "[F oBEI]".
         iMod ("VS1" $! _ V' with "[//] [$F $P //]") as (s'') "(% & T & oW)".
 
@@ -197,18 +197,18 @@ Section CAS.
 
         iSplitL "F oBEI"; last first.
           { rewrite /All_Inv.
-            rewrite (bi.big_sepS_insert _ _ _ Hs''). by iFrame. }
+            rewrite (big_sepS_insert _ _ _ Hs''). by iFrame. }
 
         rewrite /BE_Inv.
         iCombine "F" "oBEI" as "oBEI".
-        rewrite -(bi.big_sepS_insert _ _ (s'', (v_n, V'))); last first.
+        rewrite -(big_sepS_insert _ _ (s'', (v_n, V'))); last first.
           { move => In.
             by apply gset_difference_subseteq,
               subseteq_gset_filter, subseteq_gset_filter in In. }
 
         set BE':= sEx l (sBE l ({[s'', (v_n, V')]} ∪ ζ)) (s_x, (v_x, V_x)).
-        iApply (bi.big_sepS_subseteq  _ _ BE'); last first.
-        iApply (bi.big_sepS_mono _ _ (({[s'', (v_n, V')]} ∪ sEx l (sBE l ζ) (s_x, (v_x, V_x)) ∖ {[s', (v, Vr)]})) with "oBEI"); first reflexivity.
+        iApply (big_sepS_subseteq  _ _ BE'); last first.
+        iApply (big_sepS_mono _ _ (({[s'', (v_n, V')]} ∪ sEx l (sBE l ζ) (s_x, (v_x, V_x)) ∖ {[s', (v, Vr)]})) with "oBEI"); first reflexivity.
 
         set P' := λ e, (st_view (s_x, (v_x, V_x)) !! l : option positive) ⊑ st_view e !! l.
 
@@ -248,10 +248,10 @@ Section CAS.
           [by rewrite Hh'|by apply H8].
 
       (* Case: CAS fails *)
-      + rewrite /All_Inv (bi.big_sepS_delete _ _ _ InVr).
+      + rewrite /All_Inv (big_sepS_delete _ _ _ InVr).
         iDestruct "oAI" as "[Fp oAI]".
         iMod ("VSDup" $! s' v Vr with "[//] [$Fp //]") as "[Fp Fp']".
-        iCombine "Fp'" "oAI" as "oAI". rewrite -(bi.big_sepS_delete _ _ _ InVr).
+        iCombine "Fp'" "oAI" as "oAI". rewrite -(big_sepS_delete _ _ _ InVr).
         iMod (Reader_fork_Auth_2 _ _ {[s', (v, Vr)]} with "[$oA]") as "[oA #oR']".
           { by apply elem_of_subseteq_singleton. }
 
diff --git a/theories/gps/fai.v b/theories/gps/fai.v
index 1f0f3d73..f0a54646 100644
--- a/theories/gps/fai.v
+++ b/theories/gps/fai.v
@@ -87,7 +87,7 @@ Section FAI.
             + rewrite -H2 elem_of_map_gset. by exists e'.
             + exists t. by rewrite -Eq -Eq1. }
 
-      rewrite /BE_Inv (bi.big_sepS_delete _ _ _ Heb).
+      rewrite /BE_Inv (big_sepS_delete _ _ _ Heb).
       iDestruct "oBEI" as "[F oBEI]".
 
       iMod ("VS" $! v s' V' with "[//] [$F $P //]") as (s'') "(% & Q & F & Fp)".
@@ -181,18 +181,18 @@ Section FAI.
 
       iSplitL "F oBEI"; last first.
         { rewrite /All_Inv.
-          rewrite (bi.big_sepS_insert _ _ _ Hs''). by iFrame. }
+          rewrite (big_sepS_insert _ _ _ Hs''). by iFrame. }
 
       rewrite /BE_Inv.
       iCombine "F" "oBEI" as "oBEI".
-      rewrite -(bi.big_sepS_insert _ _ (s'', (v', V'))); last first.
+      rewrite -(big_sepS_insert _ _ (s'', (v', V'))); last first.
         { move => In.
           by apply gset_difference_subseteq,
             subseteq_gset_filter, subseteq_gset_filter in In. }
 
       set BE':= sEx l (sBE l ({[s'', (v', V')]} ∪ ζ)) (s_x, (v_x, V_x)).
-      iApply (bi.big_sepS_subseteq  _ _ BE'); last first.
-      iApply (bi.big_sepS_mono _ _ (({[s'', (_, V')]} ∪ sEx l (sBE l ζ) (s_x, (v_x, V_x)) ∖ {[s', (v, Vr)]})) with "oBEI"); first reflexivity.
+      iApply (big_sepS_subseteq  _ _ BE'); last first.
+      iApply (big_sepS_mono _ _ (({[s'', (_, V')]} ∪ sEx l (sBE l ζ) (s_x, (v_x, V_x)) ∖ {[s', (v, Vr)]})) with "oBEI"); first reflexivity.
 
       set P' := λ e, st_view (s_x, (v_x, V_x)) !! l ⊑ (st_view e !! l : option positive).
 
diff --git a/theories/gps/init.v b/theories/gps/init.v
index 6adbd07d..bb46f2d8 100644
--- a/theories/gps/init.v
+++ b/theories/gps/init.v
@@ -76,11 +76,11 @@ Section Init_Strong.
     - rewrite /BE_Inv.
       set ΦF := λ e, monPred_at (F γ (st_prst e) (st_val e)) (st_view e).
       rewrite (_: (monPred_at (F γ (s γ) v)) V' = ΦF ((s γ), (v, V'))); last done.
-      rewrite  -(bi.big_sepS_singleton ΦF ((s γ), (v, V'))).
-      iApply (bi.big_sepS_subseteq ΦF with "F").
+      rewrite  -(big_sepS_singleton ΦF ((s γ), (v, V'))).
+      iApply (big_sepS_subseteq ΦF with "F").
       etrans; first by apply subseteq_gset_filter.
       by apply subseteq_gset_filter.
-    - by rewrite /All_Inv bi.big_sepS_singleton.
+    - by rewrite /All_Inv big_sepS_singleton.
   Qed.
 End Init_Strong.
 
diff --git a/theories/gps/read.v b/theories/gps/read.v
index 4afbe268..a6fe3076 100644
--- a/theories/gps/read.v
+++ b/theories/gps/read.v
@@ -69,11 +69,11 @@ Section Read.
         { by apply (H0  _ _ H6 In). }
 
       iDestruct ("VS" $! s' with "[//]") as "[VS|VS]".
-      + rewrite /All_Inv (bi.big_sepS_delete _ _ _ In).
+      + rewrite /All_Inv (big_sepS_delete _ _ _ In).
         iDestruct "oAI" as "[Fp oAI]".
         iMod ("VSDup" $! _ _ Vr with "[//] [$Fp //]") as "[Fp Fp']".
         iCombine "Fp'" "oAI" as "oAI".
-        rewrite -(bi.big_sepS_delete _ _ _ In).
+        rewrite -(big_sepS_delete _ _ _ In).
         assert ((V !! l : option positive) ⊑ Vr !! l) by (rewrite H9; done).
         iMod ("VS" $! v Vr V' with "[//] [$Fp $P oA o1 Hist oBEI oAI]") as "Q".
         { repeat (iSplit; auto).
@@ -106,7 +106,7 @@ Section Read.
 
         assert (Hse : s' ⊑ st_prst e) by by apply (H0 _ _ In Ine), He.
 
-        rewrite /BE_Inv (bi.big_sepS_delete _ _ _ Heb).
+        rewrite /BE_Inv (big_sepS_delete _ _ _ Heb).
         iDestruct "oBEI" as "[F oBEI]".
         iMod ("VS" $! (st_prst e) (st_val e) Hse (V ⊔ (st_view e))
              with "[%] [$F $P]") as "[]". solve_jsl.
@@ -144,10 +144,10 @@ Section Read.
       rewrite -H2 elem_of_map_gset. by exists (s, (v, V)).
     - iNext. iIntros (v' V') "(% & kS' & Hist & % & Pure)".
       iDestruct "Pure" as (V'') "(% & % & %)".
-      rewrite /All_Inv (bi.big_sepS_delete _ _ _ H6).
+      rewrite /All_Inv (big_sepS_delete _ _ _ H6).
       iDestruct "oAI" as "[Fp oAI]".
       iMod ("VSDup" $! v V with "[//] [$Fp]") as "[Fp Fp']".
-      iCombine "Fp'" "oAI" as "oAI". rewrite -(bi.big_sepS_delete _ _ _ H6).
+      iCombine "Fp'" "oAI" as "oAI". rewrite -(big_sepS_delete _ _ _ H6).
 
       iMod (Hist_hTime_ok _ _ _ HEN with "[$kI $Hist]") as "(Hist & %)".
 
diff --git a/theories/gps/write.v b/theories/gps/write.v
index ad85cec5..b1b4f3d0 100644
--- a/theories/gps/write.v
+++ b/theories/gps/write.v
@@ -122,17 +122,17 @@ Section Write.
 
       iSplitL "F oBEI"; last first.
       + rewrite /All_Inv.
-        rewrite (bi.big_sepS_insert _ _ (s', (v, V'))) => //. by iFrame.
+        rewrite (big_sepS_insert _ _ (s', (v, V'))) => //. by iFrame.
       + rewrite /BE_Inv.
 
         iCombine "F" "oBEI" as "oBEI".
-        rewrite -(bi.big_sepS_insert _ _ (s', (v, V'))); last first.
+        rewrite -(big_sepS_insert _ _ (s', (v, V'))); last first.
           { move => In.
             by apply subseteq_gset_filter, subseteq_gset_filter in In. }
 
         set BE':= sEx l (sBE l ({[s', (v, V')]} ∪ ζ)) (s_x, (v_x, V_x)).
-        iApply (bi.big_sepS_subseteq  _ _ BE'); last first.
-        iApply (bi.big_sepS_mono _ _ ((_ ∪ sEx l (sBE l ζ) (_))) with "oBEI"); first reflexivity.
+        iApply (big_sepS_subseteq  _ _ BE'); last first.
+        iApply (big_sepS_mono _ _ ((_ ∪ sEx l (sBE l ζ) (_))) with "oBEI"); first reflexivity.
 
         set P' := λ e, st_view (s_x, (v_x, V_x)) !! l ⊑ (st_view e !! l : option positive).
 
@@ -217,7 +217,7 @@ Section Write.
           eapply (Pos.lt_le_trans); last exact Le'.
           by apply Pos.lt_add_r. }
 
-      rewrite /BE_Inv (bi.big_sepS_delete _ _ _ Heb).
+      rewrite /BE_Inv (big_sepS_delete _ _ _ Heb).
       iDestruct "oBEI" as "[F oBEI]".
 
 
@@ -289,17 +289,17 @@ Section Write.
 
       iSplitL "F oBEI"; last first.
       + rewrite /All_Inv.
-        rewrite (bi.big_sepS_insert _ _ (s', (v, V'))); last auto. by iFrame.
+        rewrite (big_sepS_insert _ _ (s', (v, V'))); last auto. by iFrame.
       + rewrite /BE_Inv.
         iCombine "F" "oBEI" as "oBEI".
-        rewrite -(bi.big_sepS_insert _ _ (s', (v, V'))); last first.
+        rewrite -(big_sepS_insert _ _ (s', (v, V'))); last first.
           { move => In.
             by apply gset_difference_subseteq,
                       subseteq_gset_filter, subseteq_gset_filter in In. }
 
         set BE':= sEx l (sBE l ({[s', (v, V')]} ∪ ζ)) (s', (v, V')).
-        iApply (bi.big_sepS_subseteq  _ _ BE'); last first.
-        iApply (bi.big_sepS_mono _ _ ({[s', (v, V')]} ∪ sEx l (sBE l ζ) (s_x, (v_x, V_x)) ∖ {[s_x, (v_x, V_x)]}) with "oBEI"); first reflexivity.
+        iApply (big_sepS_subseteq  _ _ BE'); last first.
+        iApply (big_sepS_mono _ _ ({[s', (v, V')]} ∪ sEx l (sBE l ζ) (s_x, (v_x, V_x)) ∖ {[s_x, (v_x, V_x)]}) with "oBEI"); first reflexivity.
 
         etrans; last apply union_subseteq_l.
         rewrite /BE'.
diff --git a/theories/iris_lemmas.v b/theories/iris_lemmas.v
index fea8499b..3025ffe1 100644
--- a/theories/iris_lemmas.v
+++ b/theories/iris_lemmas.v
@@ -12,11 +12,11 @@ Section Extra.
       ⊢ φ s ∗ ([∗ set] s' ∈ S, φ s').
   Proof.
     iIntros "(Dup & ress)".
-    rewrite {1}(bi.big_sepS_delete _ _ _ In).
+    rewrite {1}(big_sepS_delete _ _ _ In).
     iDestruct "ress" as "(Hφd & ress)".
     iDestruct ("Dup" with "Hφd") as "(Hφd1 & ?)".
     iCombine "Hφd1" "ress" as "ress".
-    rewrite -(bi.big_sepS_delete _ _ _ In).
+    rewrite -(big_sepS_delete _ _ _ In).
     by iFrame.
   Qed.
 
diff --git a/theories/malloc.v b/theories/malloc.v
index c3cd4173..62faeaca 100644
--- a/theories/malloc.v
+++ b/theories/malloc.v
@@ -152,7 +152,7 @@ Section proof.
 
     iAssert (([∗ list] i ∈ seq 0 (Z.to_nat z), ZplusPos (Z.of_nat i) l ↦ ?))
       with "[oL]" as "Big".
-    { rewrite -Eqz bi.big_sepL_singleton. iDestruct "oL" as (h) "oL". by iExists _. }
+    { rewrite -Eqz big_sepL_singleton. iDestruct "oL" as (h) "oL". by iExists _. }
 
     clear Eqz Eqmax.
 
@@ -177,7 +177,7 @@ Section proof.
           [omega..|].
 
         rewrite Z2Nat.inj_succ; last omega.
-        rewrite seq_S big_opL_app bi.big_sepL_singleton.
+        rewrite seq_S big_opL_app big_sepL_singleton.
         iFrame "Big".
         rewrite /= Z2Nat.id; last omega.
         iDestruct "oL" as (h) "oL".
-- 
GitLab