From 3161ebb24737c711acced49713695a3414ac0a90 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 21 Mar 2017 13:14:52 +0100
Subject: [PATCH] Update to new big ops in Iris.

---
 opam.pins                                 |  2 +-
 theories/lang/heap.v                      | 19 +++++++++----------
 theories/lang/lifting.v                   | 20 +++++++++-----------
 theories/lifetime/model/raw_reborrow.v    |  2 +-
 theories/typing/borrow.v                  |  5 ++---
 theories/typing/function.v                |  8 ++++----
 theories/typing/lft_contexts.v            |  8 ++------
 theories/typing/lib/refcell/ref_code.v    |  8 +++++---
 theories/typing/lib/refcell/refmut_code.v |  8 +++++---
 theories/typing/lib/spawn.v               |  2 +-
 theories/typing/own.v                     |  7 ++++---
 theories/typing/product_split.v           |  4 ++--
 theories/typing/programs.v                |  4 ++--
 theories/typing/shr_bor.v                 |  6 +++---
 theories/typing/soundness.v               |  4 ++--
 theories/typing/type_context.v            | 13 +++++--------
 16 files changed, 57 insertions(+), 63 deletions(-)

diff --git a/opam.pins b/opam.pins
index 0939fcaa..3581188d 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq a378b8288ebab8d6d16afe0864453731bd753a1d
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq e906ef70877d20c63a36f791a9d6620b613695a8
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 1bc07739..65b01d93 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -1,7 +1,7 @@
 From Coq Require Import Min.
 From stdpp Require Import coPset.
-From iris.algebra Require Import cmra_big_op gmap frac agree.
-From iris.algebra Require Import csum excl auth.
+From iris.algebra Require Import big_op gmap frac agree.
+From iris.algebra Require Import csum excl auth cmra_big_op.
 From iris.base_logic Require Import big_op lib.fractional.
 From iris.base_logic Require Export lib.own.
 From iris.proofmode Require Export tactics.
@@ -147,7 +147,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
-  Proof. by rewrite /heap_mapsto_vec big_sepL_nil. Qed.
+  Proof. by rewrite /heap_mapsto_vec. Qed.
 
   Lemma heap_mapsto_vec_app l q vl1 vl2 :
     l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ shift_loc l (length vl1) ↦∗{q} vl2.
@@ -157,7 +157,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_vec_singleton l q v : l ↦∗{q} [v] ⊣⊢ l ↦{q} v.
-  Proof. by rewrite /heap_mapsto_vec big_sepL_singleton /= shift_loc_0. Qed.
+  Proof. by rewrite /heap_mapsto_vec /= shift_loc_0 right_id. Qed.
 
   Lemma heap_mapsto_vec_cons l q v vl:
     l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ shift_loc l 1 ↦∗{q} vl.
@@ -204,7 +204,7 @@ Section heap.
 
   Lemma heap_mapsto_vec_combine l q vl :
     vl ≠ [] →
-    l ↦∗{q} vl ⊣⊢ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
+    l ↦∗{q} vl ⊣⊢ own heap_name (◯ [^op list] i ↦ v ∈ vl,
       {[shift_loc l i := (q, Cinr 0%nat, to_agree v)]}).
   Proof.
     rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
@@ -335,7 +335,7 @@ Section heap.
     (∀ m : Z, σ !! shift_loc l m = None) →
     own heap_name (● to_heap σ)
     ==∗ own heap_name (● to_heap (init_mem l vl σ))
-       ∗ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
+       ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
            {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]}).
   Proof.
     intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
@@ -374,7 +374,7 @@ Section heap.
   Qed.
 
   Lemma heap_free_vs σ l vl :
-    own heap_name (● to_heap σ) ∗ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
+    own heap_name (● to_heap σ) ∗ own heap_name (◯ [^op list] i ↦ v ∈ vl,
       {[shift_loc l i := (1%Qp, Cinr 0%nat, to_agree v)]})
     ==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
   Proof.
@@ -382,9 +382,8 @@ Section heap.
     revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
     rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /= shift_loc_0.
     apply local_update_total_valid=> _ Hvalid _.
-    assert (([⋅ list] k↦y ∈ vl,
-      {[shift_loc l (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]}) !! l
-      = @None (frac * lock_stateR * agree valC)).
+    assert (([^op list] k↦y ∈ vl,
+      {[shift_loc l (1 + k) := (1%Qp, Cinr 0%nat, to_agree y)]} : heapUR) !! l = None).
     { move: (Hvalid l). rewrite lookup_op lookup_singleton.
       by move=> /(cmra_discrete_valid_iff 0) /exclusiveN_Some_l. }
     rewrite -insert_singleton_op //. etrans.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index faa9932c..bea9a136 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -89,7 +89,7 @@ Proof.
   iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
-  iModIntro. iFrame "Hσ". iSplit; [|by iApply big_sepL_nil].
+  iModIntro. iFrame "Hσ". iSplit; last done.
   clear dependent σ1 n.
   iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iMod ("Hσclose" with "Hσ") as (n) "(% & Hσ & Hv)".
@@ -122,7 +122,7 @@ Proof.
   iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
-  iModIntro. iFrame "Hσ". iSplit; [|by iApply big_sepL_nil].
+  iModIntro. iFrame "Hσ". iSplit; last done.
   clear dependent σ1. iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ". iMod ("Hσclose" with "Hσ") as "(% & Hσ & Hv)".
   iModIntro; iSplit; first by eauto.
@@ -261,7 +261,7 @@ Proof.
   iIntros (? Φ) "HΦ". iApply wp_lift_pure_head_step; eauto.
   { intros. by inv_head_step. }
   iApply step_fupd_intro; first done. iNext. iIntros (e2 efs σ Hs).
-  inv_head_step; rewrite big_sepL_nil right_id.
+  inv_head_step; rewrite right_id.
   rewrite -wp_value //. iApply "HΦ". eauto.
 Qed.
 
@@ -337,16 +337,16 @@ Lemma wp_app_ind E f (el : list expr) (Ql : vec (val → iProp Σ) (length el))
                     WP App f (of_val <$> vs ++ vl) @ E {{ Φ }}) -∗
     WP App f ((of_val <$> vs) ++ el) @ E {{ Φ }}.
 Proof.
-  intros [vf Hf]. revert vs Ql. induction el as [|e el IH]=>/= vs Ql; inv_vec Ql.
-  - iIntros "_ H". iSpecialize ("H" $! [#]). rewrite !app_nil_r big_sepL_nil.
-      by iApply "H".
-  - intros Q Ql. rewrite /= big_sepL_cons /=. iIntros "[He Hl] HΦ".
+  intros [vf Hf]. revert vs Ql.
+  induction el as [|e el IH]=>/= vs Ql; inv_vec Ql; simpl.
+  - iIntros "H". iSpecialize ("H" $! [#]). rewrite !app_nil_r /=. by iApply "H".
+  - iIntros (Q Ql) "[He Hl] HΦ".
     assert (App f ((of_val <$> vs) ++ e :: el) = fill_item (AppRCtx vf vs el) e)
       as -> by rewrite /= (of_to_val f) //.
     iApply wp_bindi. iApply (wp_wand with "He"). iIntros (v) "HQ /=".
     rewrite cons_middle (assoc app) -(fmap_app _ _ [v]) (of_to_val f) //.
     iApply (IH _ _ with "Hl"). iIntros "* Hvl". rewrite -assoc.
-    iApply ("HΦ" $! (v:::vl)). rewrite /= big_sepL_cons. iFrame.
+    iApply ("HΦ" $! (v:::vl)). iFrame.
 Qed.
 
 Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
@@ -355,9 +355,7 @@ Lemma wp_app_vec E f el (Ql : vec (val → iProp Σ) (length el)) Φ :
     (∀ vl : vec val (length el), ([∗ list] vQ ∈ zip vl Ql, vQ.2 $ vQ.1) -∗
                     WP App f (of_val <$> (vl : list val)) @ E {{ Φ }}) -∗
     WP App f el @ E {{ Φ }}.
-Proof.
-  iIntros (Hf). iApply (wp_app_ind _ _ _ _ []). done.
-Qed.
+Proof. iIntros (Hf). by iApply (wp_app_ind _ _ _ _ []). Qed.
 
 Lemma wp_app (Ql : list (val → iProp Σ)) E f el Φ :
   length Ql = length el → is_Some (to_val f) →
diff --git a/theories/lifetime/model/raw_reborrow.v b/theories/lifetime/model/raw_reborrow.v
index fadea3d2..78be6b25 100644
--- a/theories/lifetime/model/raw_reborrow.v
+++ b/theories/lifetime/model/raw_reborrow.v
@@ -88,7 +88,7 @@ Proof.
      as "Hbox"; first by solve_ndisj.
   { by rewrite lookup_fmap HB. }
   iDestruct (@big_sepM_delete with "HB") as "[Hcnt HB]"; first done.
-  rewrite /=; iDestruct "Hcnt" as "[% H1â—¯]".
+  rewrite /=. iDestruct "Hcnt" as "[% H1â—¯]".
   iMod ("Hvs" $! I with "[Hκdead' HI Hinv Hvs' Hinh HB● Hbox HB]
                          [$HPb Hi] Hκ†") as "($ & $ & Hcnt')".
   { rewrite lft_vs_inv_unfold. iFrame "Hκdead' HI".
diff --git a/theories/typing/borrow.v b/theories/typing/borrow.v
index e97f2447..d3f7b676 100644
--- a/theories/typing/borrow.v
+++ b/theories/typing/borrow.v
@@ -15,11 +15,10 @@ Section borrow.
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [p ◁ own_ptr n ty] [p ◁ &uniq{κ}ty; p ◁{κ} own_ptr n ty].
   Proof.
-    iIntros (tid ?)  "#LFT _ $ H".
-    rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iIntros (tid ?)  "#LFT _ $ [H _]".
     iDestruct "H" as ([[]|]) "[% Hown]"; try done. iDestruct "Hown" as "[Hmt ?]".
     iMod (bor_create with "LFT Hmt") as "[Hbor Hext]". done.
-    iModIntro. iSplitL "Hbor".
+    iModIntro. rewrite /tctx_interp /=. iSplitL "Hbor"; last iSplit; last done.
     - iExists _. auto.
     - iExists _. iSplit. done. by iFrame.
   Qed.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index b788a600..68d951e7 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -246,15 +246,15 @@ Section typing.
     iApply (wp_app_vec _ _ (_::_) ((λ v, ⌜v = (λ: ["_r"], (#() ;; #()) ;; k ["_r"])%V⌝):::
                vmap (λ ty (v : val), tctx_elt_interp tid (v ◁ box ty)) (fp x).(fp_tys))%I
             with "[Hargs]"); first wp_done.
-    - rewrite /= big_sepL_cons. iSplitR "Hargs".
+    - rewrite /=. iSplitR "Hargs".
       { simpl. iApply wp_value; last done. solve_to_val. }
       clear dependent k p.
       rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
               (zip_with_zip (λ e ty, (e, _))) zip_with_zip !big_sepL_fmap.
-      iApply (big_sepL_mono' with "Hargs"). iIntros (i [p ty]) "HT/=".
+      iApply (big_sepL_mono' with "Hargs"); last done. iIntros (i [p ty]) "HT/=".
       iApply (wp_hasty with "HT"). setoid_rewrite tctx_hasty_val. iIntros (?) "? $".
     - simpl. change (@length expr ps) with (length ps).
-      iIntros (vl'). inv_vec vl'=>kv vl. rewrite /= big_sepL_cons.
+      iIntros (vl'). inv_vec vl'=>kv vl.
       iIntros "/= [% Hvl]". subst kv. iDestruct "Hf" as (fb kb xb e ?) "[EQ [EQl #Hf]]".
       iDestruct "EQ" as %[=->]. iDestruct "EQl" as %EQl. revert vl fp HE.
       rewrite <-EQl=>vl fp HE. iApply wp_rec; try done.
@@ -281,7 +281,7 @@ Section typing.
         rewrite tctx_interp_singleton tctx_interp_cons. iFrame.
       + rewrite /tctx_interp vec_to_list_map !zip_with_fmap_r
                 (zip_with_zip (λ v ty, (v, _))) zip_with_zip !big_sepL_fmap.
-        iApply (big_sepL_mono' with "Hvl"). by iIntros (i [v ty']).
+        iApply (big_sepL_mono' with "Hvl"); last done. by iIntros (i [v ty']).
   Qed.
 
   Lemma type_call {A} x E L C T T' T'' p (ps : list path)
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index 5c16ddf5..b5359302 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -267,9 +267,7 @@ Section lft_contexts.
     ∀ qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ elctx_interp E').
 
   Lemma elctx_sat_nil : elctx_sat [].
-  Proof.
-    iIntros (?) "_ !# _". rewrite /elctx_interp big_sepL_nil. auto.
-  Qed.
+  Proof. iIntros (?) "_ !# _". by rewrite /elctx_interp /=. Qed.
 
   Lemma elctx_sat_lft_incl E' κ κ' :
     lctx_lft_incl κ κ' → elctx_sat E' → elctx_sat ((κ ⊑ κ') :: E')%EL.
@@ -277,9 +275,7 @@ Section lft_contexts.
     iIntros (Hκκ' HE' qL) "HL".
     iDestruct (Hκκ' with "HL") as "#Hincl".
     iDestruct (HE' with "HL") as "#HE'".
-    iClear "∗". iIntros "!# #HE".
-    (* FIXME: Why does iSplit fail here?  The goal is persistent. *)
-    iSplitL.
+    iClear "∗". iIntros "!# #HE". iSplit.
     - by iApply "Hincl".
     - by iApply "HE'".
   Qed.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 9f7c86c5..4f65c7b1 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -250,7 +250,8 @@ Section ref_functions.
        with "[] LFT [] Hna HL [-H† Hlx Henv]"); swap 1 2; swap 3 4.
     { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
     { iApply (type_call (α ⊓ ν)); solve_typing. }
-    { iFrame "∗#". iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
+    { rewrite /tctx_interp /=. iFrame "Hf' Henv".
+      iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
       iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto. }
     iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
     apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
@@ -266,13 +267,14 @@ Section ref_functions.
     iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
     wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
       first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
-    iApply (type_type _ _ _
+    iApply (type_type _ [_] _
         [ f ◁ box (fn(∀ α, ∅; envty, &shr{α}ty1) → &shr{α}ty2);
           #lref ◁ box (ref α ty2) ]%TC
-       with "[] LFT HE Hna HL Hk"); first last.
+       with "[] LFT HE Hna [HL] Hk"); first last.
     { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
       iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
+    { rewrite /llctx_interp /=; auto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index e2649e7c..0333b59c 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -203,7 +203,8 @@ Section refmut_functions.
        with "[] LFT [] Hna HL [-H† Hlx Henv Hbor]"); swap 1 2; swap 3 4.
     { iSplitL; last iSplitL; [done|iApply lft_intersect_incl_l|iApply "HE"]. }
     { iApply (type_call (α ⊓ ν)); solve_typing. }
-    { iFrame "∗#". iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
+    { rewrite /tctx_interp /=. iFrame "Hf' Henv".
+      iApply tctx_hasty_val'; first done. rewrite -freeable_sz_full.
       iFrame. iExists [_]. rewrite heap_mapsto_vec_singleton. auto with iFrame. }
     iIntros (? ->%elem_of_list_singleton arg) "Hna HL Hr". inv_vec arg=>r.
     apply of_to_val in EQk. rewrite EQk. iApply wp_rec; try (done || apply _).
@@ -219,13 +220,14 @@ Section refmut_functions.
     iApply wp_mask_mono; last iApply (wp_step_fupd with "Hκ'†"); auto with ndisj.
     wp_seq. iIntros "Hκ'† !>". iMod ("Hν" with "[Hκ'†]") as "Hν";
       first by rewrite -lft_dead_or; auto. wp_seq. wp_write.
-    iApply (type_type _ _ _
+    iApply (type_type _ [_] _
         [ f ◁ box (fn(∀ α, ∅; envty, &uniq{α}ty1) → &uniq{α}ty2);
           #lref ◁ box (refmut α ty2) ]%TC
-       with "[] LFT HE Hna HL Hk"); first last.
+       with "[] LFT HE Hna [HL] Hk"); first last.
     { iFrame. rewrite big_sepL_singleton tctx_hasty_val. iExists _. iSplit. done.
       iFrame. iExists [_;_]. rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
       iFrame. destruct r' as [[]|]=>//=. auto 10 with iFrame. }
+    { rewrite /llctx_interp /=; auto. }
     iApply type_delete; [solve_typing..|].
     iApply type_jump; solve_typing.
   Qed.
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index d2a67fab..d6a4140f 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -96,7 +96,7 @@ Section spawn.
       iApply (Hcall with "LFT HE Htl [] [Hfin]").
       - constructor.
       - solve_typing.
-      - rewrite /llctx_interp big_sepL_nil. done.
+      - by rewrite /llctx_interp /=.
       - rewrite /cctx_interp. iIntros "* Hin".
         iDestruct "Hin" as %Hin%elem_of_list_singleton. subst x.
         rewrite /cctx_elt_interp. iIntros "* ?? Hret". inv_vec args=>arg /=.
diff --git a/theories/typing/own.v b/theories/typing/own.v
index 1fee0f12..8d01d9ad 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -286,9 +286,10 @@ Section typing.
     iIntros (<- tid) "#LFT #HE $ $ Hp". rewrite tctx_interp_singleton.
     wp_bind p. iApply (wp_hasty with "Hp"). iIntros ([[]|]) "_ Hown"; try done.
     iDestruct "Hown" as "[H↦: >H†]". iDestruct "H↦:" as (vl) "[>H↦ Hown]".
-    rewrite tctx_interp_nil. iDestruct (ty_size_eq with "Hown") as "#>EQ".
-    iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto; [].
-    rewrite freeable_sz_full. by iFrame.
+    iDestruct (ty_size_eq with "Hown") as "#>EQ".
+    iDestruct "EQ" as %<-. iApply (wp_delete with "[-]"); auto.
+    - iFrame "H↦". by iApply freeable_sz_full.
+    - rewrite /tctx_interp /=; auto.
   Qed.
 
   Lemma type_delete {E L} ty C T T' (n' : nat) (n : Z)  p e :
diff --git a/theories/typing/product_split.v b/theories/typing/product_split.v
index 68d42dba..4f54c80e 100644
--- a/theories/typing/product_split.v
+++ b/theories/typing/product_split.v
@@ -41,13 +41,13 @@ Section product_split.
     iInduction tyl as [|ty tyl IH] "IH" forall (p).
     { rewrite tctx_interp_nil. auto. }
     rewrite product_cons. iMod (Hsplit with "LFT HE HL H") as "(HL & H)".
-    cbn -[tctx_elt_interp]. rewrite tctx_interp_cons tctx_interp_singleton tctx_interp_cons.
+    cbn -[tctx_elt_interp].
     iDestruct "H" as "[Hty Htyl]". iDestruct "Hty" as (v) "[Hp Hty]". iDestruct "Hp" as %Hp. 
     iDestruct (Hloc with "Hty") as %[l [=->]].
     iAssert (tctx_elt_interp tid (p +ₗ #0 ◁ ptr ty)) with "[Hty]" as "$".
     { iExists #l. iSplit; last done. simpl; by rewrite Hp shift_loc_0. }
     iMod ("IH" with "HL [Htyl]") as "($ & Htyl)".
-    { rewrite tctx_interp_singleton //. }
+    { auto. }
     iClear "IH". rewrite (hasty_ptr_offsets_offset l) // -plus_n_O //.
   Qed.
 
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index 7f545608..372bb223 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -103,7 +103,7 @@ Section typing_rules.
     rewrite /llctx_interp big_sepL_cons. iDestruct "HL" as "[Hκ HL]".
     iMod (lctx_equalize_lft with "LFT Hκ") as "[Hκ1 Hκ2]".
     iApply (He with "LFT [Hκ1 Hκ2 HE] Htl HL HC HT").
-    rewrite /elctx_interp !big_sepL_cons. by iFrame.
+    rewrite /elctx_interp /=. by iFrame.
   Qed.
 
   Lemma type_let' E L T1 T2 (T : tctx) C xb e e' :
@@ -153,7 +153,7 @@ Section typing_rules.
     iMod (lft_create with "LFT") as (Λ) "[Htk #Hinh]"; first done.
     set (κ' := lft_intersect_list κs). wp_seq.
     iApply ("He" $! (κ' ⊓ Λ) with "LFT HE Htl [HL Htk] HC HT").
-    rewrite /llctx_interp big_sepL_cons. iFrame "HL".
+    rewrite /llctx_interp /=. iFrame "HL".
     iExists Λ. iSplit; first done. iFrame. done.
   Qed.
 
diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index a7cad9b8..8d52bd5f 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -69,11 +69,11 @@ Section typing.
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [p ◁ &shr{κ}ty] [p ◁ &shr{κ'}ty; p ◁{κ} &shr{κ}ty].
   Proof.
-    iIntros (Hκκ' tid ?) "#LFT #HE HL H". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
-    iFrame. rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
+    iIntros (Hκκ' tid ?) "#LFT #HE HL [H _]". iDestruct (Hκκ' with "HL HE") as "#Hκκ'".
+    iFrame. rewrite /tctx_interp /=.
     iDestruct "H" as ([[]|]) "[% #Hshr]"; try done. iModIntro. iSplit.
     - iExists _. iSplit. done. by iApply (ty_shr_mono with "Hκκ' Hshr").
-    - iExists _. auto.
+    - iSplit=> //. iExists _. auto.
   Qed.
 
   Lemma read_shr E L κ ty :
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 42ba0dbb..88a0a46a 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -53,8 +53,8 @@ Section type_soundness.
     iMod (lft_create with "LFT") as (ϝ) "Hϝ". done.
     iApply ("Hmain" $! () ϝ exit_cont [#] tid with "LFT [] Htl [Hϝ] []");
       last by rewrite tctx_interp_nil.
-    { by rewrite /elctx_interp /= big_sepL_nil. }
-    { rewrite /llctx_interp big_sepL_singleton. iExists ϝ. iFrame. by rewrite /= left_id. }
+    { by rewrite /elctx_interp /=. }
+    { rewrite /llctx_interp /=. iSplit; last done. iExists ϝ. iFrame. by rewrite /= left_id. }
     rewrite cctx_interp_singleton. simpl. iIntros (args) "_ _".
     inv_vec args. iIntros (x) "_ /=". by wp_lam.
   Qed.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 077f13ce..e31f4870 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -130,7 +130,7 @@ Section type_context.
 
   Lemma tctx_interp_cons tid x T :
     tctx_interp tid (x :: T) ≡ (tctx_elt_interp tid x ∗ tctx_interp tid T)%I.
-  Proof. rewrite /tctx_interp big_sepL_cons //. Qed.
+  Proof. done. Qed.
 
   Lemma tctx_interp_app tid T1 T2 :
     tctx_interp tid (T1 ++ T2) ≡ (tctx_interp tid T1 ∗ tctx_interp tid T2)%I.
@@ -141,7 +141,7 @@ Section type_context.
 
   Lemma tctx_interp_singleton tid x :
     tctx_interp tid [x] ≡ tctx_elt_interp tid x.
-  Proof. rewrite tctx_interp_cons tctx_interp_nil right_id //. Qed.
+  Proof. rewrite /tctx_interp /= right_id //. Qed.
 
   (** Copy typing contexts *)
   Class CopyC (T : tctx) :=
@@ -216,10 +216,7 @@ Section type_context.
 
   Lemma copy_tctx_incl E L p `{!Copy ty} :
     tctx_incl E L [p ◁ ty] [p ◁ ty; p ◁ ty].
-  Proof.
-    iIntros (??) "_ _ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
-    by iIntros "[#$ $]".
-  Qed.
+  Proof. iIntros (??) "_ _ $ * [#$ $] //". Qed.
 
   Lemma copy_elem_of_tctx_incl E L T p `{!Copy ty} :
     (p ◁ ty)%TC ∈ T → tctx_incl E L T ((p ◁ ty) :: T).
@@ -233,9 +230,9 @@ Section type_context.
   Lemma subtype_tctx_incl E L p ty1 ty2 :
     subtype E L ty1 ty2 → tctx_incl E L [p ◁ ty1] [p ◁ ty2].
   Proof.
-    iIntros (Hst ??) "#LFT #HE HL H". rewrite /tctx_interp !big_sepL_singleton /=.
+    iIntros (Hst ??) "#LFT #HE HL [H _]".
     iDestruct "H" as (v) "[% H]". iDestruct (Hst with "HL HE") as "#(_ & Ho & _)". 
-    iFrame "HL". iExists _. iFrame "%". by iApply "Ho".
+    iFrame "HL". iApply big_sepL_singleton. iExists _. iFrame "%". by iApply "Ho".
   Qed.
 
   (* Extracting from a type context. *)
-- 
GitLab