From b632359ea8636843dba9166e7699b14e870e49e5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 3 May 2023 22:01:22 +0200
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam                   |  2 +-
 theories/lang/heap.v                   | 12 ++++++------
 theories/lang/lifting.v                |  8 ++++----
 theories/lang/proofmode.v              | 12 ++++++------
 theories/lifetime/at_borrow.v          |  6 +++++-
 theories/lifetime/model/primitive.v    | 14 +++++++-------
 theories/typing/fixpoint.v             |  2 +-
 theories/typing/lft_contexts.v         |  6 +++---
 theories/typing/lib/arc.v              |  4 ++--
 theories/typing/lib/mutex/mutexguard.v |  3 ++-
 theories/typing/programs.v             |  2 +-
 theories/typing/sum.v                  |  2 +-
 theories/typing/type.v                 | 18 +++++++++---------
 theories/typing/type_context.v         |  2 +-
 14 files changed, 49 insertions(+), 44 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index a1facd94..efa91425 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
+  "coq-iris" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index e3f918db..ef1051a5 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -348,7 +348,7 @@ Section heap.
        ∗ own heap_name (◯ [^op list] i ↦ v ∈ (repeat (LitV LitPoison) n),
            {[l +â‚— i := (1%Qp, Cinr 0%nat, to_agree v)]}).
   Proof.
-    intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
+    intros FREE. rewrite -own_op. apply entails_wand, own_update, auth_update_alloc.
     revert l FREE. induction n as [|n IH]=> l FRESH; [done|].
     rewrite (big_opL_consZ_l (λ k _, _ (_ k) _ )) /=.
     etrans; first apply (IH (l +â‚— 1)).
@@ -389,7 +389,7 @@ Section heap.
       {[l +â‚— i := (1%Qp, Cinr 0%nat, to_agree v)]})
     ==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
   Proof.
-    rewrite -own_op. apply own_update, auth_update_dealloc.
+    rewrite -own_op. apply entails_wand, own_update, auth_update_dealloc.
     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 _.
@@ -469,8 +469,8 @@ Section heap.
     ==∗ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
         ∗ heap_mapsto_st (RSt n2) l q v.
   Proof.
-    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
-    eapply own_update, auth_update, singleton_local_update.
+    intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
+    iApply own_update. eapply auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply prod_local_update_1, prod_local_update_2, csum_local_update_r.
     apply nat_local_update; lia.
@@ -518,8 +518,8 @@ Section heap.
     ==∗ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
         ∗ heap_mapsto_st st2 l 1%Qp v'.
   Proof.
-    intros Hσv. apply wand_intro_r. rewrite -!own_op to_heap_insert.
-    eapply own_update, auth_update, singleton_local_update.
+    intros Hσv. apply entails_wand, wand_intro_r. rewrite -!own_op to_heap_insert.
+    iApply own_update. eapply auth_update, singleton_local_update.
     { by rewrite /to_heap lookup_fmap Hσv. }
     apply exclusive_local_update. by destruct st2.
   Qed.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index ae3b1cb4..9de46d59 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -303,10 +303,10 @@ Proof.
 Qed.
 
 Lemma wp_eq_loc E (l1 : loc) (l2: loc) q1 q2 v1 v2 P Φ :
-  (P -∗ ▷ l1 ↦{q1} v1) →
-  (P -∗ ▷ l2 ↦{q2} v2) →
-  (P -∗ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
-  P -∗ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
+  (P ⊢ ▷ l1 ↦{q1} v1) →
+  (P ⊢ ▷ l2 ↦{q2} v2) →
+  (P ⊢ ▷ Φ (LitV (bool_decide (l1 = l2)))) →
+  P ⊢ WP BinOp EqOp (Lit (LitLoc l1)) (Lit (LitLoc l2)) @ E {{ Φ }}.
 Proof.
   iIntros (Hl1 Hl2 Hpost) "HP".
   destruct (bool_decide_reflect (l1 = l2)) as [->|].
diff --git a/theories/lang/proofmode.v b/theories/lang/proofmode.v
index 916bc9a2..47b82736 100644
--- a/theories/lang/proofmode.v
+++ b/theories/lang/proofmode.v
@@ -105,7 +105,7 @@ Lemma tac_wp_alloc K Δ Δ' E j1 j2 n Φ :
   envs_entails Δ (WP fill K (Alloc (Lit $ LitInt n)) @ E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal=> ?? HΔ. rewrite -wp_bind.
-  eapply wand_apply; first exact:wp_alloc.
+  eapply wand_apply; first by apply wand_entails, wp_alloc.
   rewrite -persistent_and_sep. apply and_intro; first by auto.
   rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
   apply forall_intro=>sz. apply wand_intro_l. rewrite -assoc.
@@ -126,7 +126,7 @@ Lemma tac_wp_free K Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   envs_entails Δ (WP fill K (Free (Lit $ LitInt n) (Lit $ LitLoc l)) @ E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal; intros -> ?? <- ? <- -> HΔ. rewrite -wp_bind.
-  eapply wand_apply; first exact:wp_free; simpl.
+  eapply wand_apply; first by apply wand_entails, wp_free; simpl.
   rewrite into_laterN_env_sound -!later_sep; apply later_mono.
   do 2 (rewrite envs_lookup_sound //). by rewrite HΔ True_emp emp_wand -assoc.
 Qed.
@@ -139,10 +139,10 @@ Lemma tac_wp_read K Δ Δ' E i l q v o Φ :
   envs_entails Δ (WP fill K (Read o (Lit $ LitLoc l)) @ E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal; intros [->| ->] ???.
-  - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_na.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_read_na.
     rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
     by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_bind. eapply wand_apply; first exact:wp_read_sc.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_read_sc.
     rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
     by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -157,10 +157,10 @@ Lemma tac_wp_write K Δ Δ' Δ'' E i l v e v' o Φ :
   envs_entails Δ (WP fill K (Write o (Lit $ LitLoc l) e) @ E {{ Φ }}).
 Proof.
   rewrite envs_entails_unseal; intros ? [->| ->] ????.
-  - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_na.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_write_na.
     rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_bind. eapply wand_apply; first by apply wp_write_sc.
+  - rewrite -wp_bind. eapply wand_apply; first by apply wand_entails, wp_write_sc.
     rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 8f67ef3f..d1c372d8 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -101,6 +101,10 @@ Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ userE} (P : iProp Σ) E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
              [†κ] ∗ |={E∖↑lftN,E}=> True.
-Proof. intros. by rewrite (at_bor_acc _ lftN) // difference_twice_L. Qed.
+Proof.
+  iIntros (?) "H".
+  iDestruct (at_bor_acc _ lftN with "H") as "H"; [done..|].
+  by rewrite difference_twice_L.
+Qed.
 
 Global Typeclasses Opaque at_bor.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 51db9d35..4c5d7294 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -77,7 +77,7 @@ Qed.
 Lemma own_bor_valid κ x : own_bor κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_bor_valid_2 κ x y : own_bor κ x -∗ own_bor κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_bor_op. apply own_bor_valid. Qed.
+Proof. apply entails_wand, wand_intro_r. rewrite -own_bor_op. iApply own_bor_valid. Qed.
 Global Instance own_bor_sep_gives κ x y :
   CombineSepGives (own_bor κ x) (own_bor κ y) (✓ (x ⋅ y)).
 Proof.
@@ -92,7 +92,7 @@ Qed.
 Lemma own_bor_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_bor κ x1 ⊢ own_bor κ x2 ==∗ own_bor κ y.
 Proof.
-  intros. apply wand_intro_r. rewrite -own_bor_op. by apply own_bor_update.
+  intros. apply wand_intro_r. rewrite -own_bor_op. by iApply own_bor_update.
 Qed.
 
 Lemma own_cnt_auth I κ x : own_ilft_auth I -∗ own_cnt κ x -∗ ⌜is_Some (I !! κ)⌝.
@@ -118,7 +118,7 @@ Qed.
 Lemma own_cnt_valid κ x : own_cnt κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_cnt_valid_2 κ x y : own_cnt κ x -∗ own_cnt κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_cnt_op. apply own_cnt_valid. Qed.
+Proof. apply entails_wand, wand_intro_r. rewrite -own_cnt_op. iApply own_cnt_valid. Qed.
 Global Instance own_cnt_sep_gives κ x y :
   CombineSepGives (own_cnt κ x) (own_cnt κ y) (✓ (x ⋅ y)).
 Proof.
@@ -132,7 +132,7 @@ Qed.
 Lemma own_cnt_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_cnt κ x1 -∗ own_cnt κ x2 ==∗ own_cnt κ y.
 Proof.
-  intros. apply wand_intro_r. rewrite -own_cnt_op. by apply own_cnt_update.
+  intros. apply entails_wand, wand_intro_r. rewrite -own_cnt_op. by iApply own_cnt_update.
 Qed.
 
 Lemma own_inh_auth I κ x : own_ilft_auth I -∗ own_inh κ x -∗ ⌜is_Some (I !! κ)⌝.
@@ -158,7 +158,7 @@ Qed.
 Lemma own_inh_valid κ x : own_inh κ x -∗ ✓ x.
 Proof. iDestruct 1 as (γs) "[#? Hx]". by iApply own_valid. Qed.
 Lemma own_inh_valid_2 κ x y : own_inh κ x -∗ own_inh κ y -∗ ✓ (x ⋅ y).
-Proof. apply wand_intro_r. rewrite -own_inh_op. apply own_inh_valid. Qed.
+Proof. apply entails_wand, wand_intro_r. rewrite -own_inh_op. iApply own_inh_valid. Qed.
 Global Instance own_inh_sep_gives κ x y :
   CombineSepGives (own_inh κ x) (own_inh κ y) (✓ (x ⋅ y)).
 Proof.
@@ -172,7 +172,7 @@ Qed.
 Lemma own_inh_update_2 κ x1 x2 y :
   x1 ⋅ x2 ~~> y → own_inh κ x1 ⊢ own_inh κ x2 ==∗ own_inh κ y.
 Proof.
-  intros. apply wand_intro_r. rewrite -own_inh_op. by apply own_inh_update.
+  intros. apply wand_intro_r. rewrite -own_inh_op. by iApply own_inh_update.
 Qed.
 
 (** Alive and dead *)
@@ -359,7 +359,7 @@ Qed.
 Lemma lft_incl_intro κ κ' :
   □ ((∀ q, q.[κ] ={↑lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={↑lftN}=∗ q.[κ])) ∗
       ([†κ'] ={↑lftN}=∗ [†κ])) -∗ κ ⊑ κ'.
-Proof. reflexivity. Qed.
+Proof. iIntros "?". done. Qed.
 
 Lemma lft_intersect_incl_l κ κ' : ⊢ κ ⊓ κ' ⊑ κ.
 Proof.
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index b78bed96..fcf76026 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -61,7 +61,7 @@ Section fixpoint.
       { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
       apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
       + apply bi.limit_preserving_Persistent; solve_proper.
-      + apply limit_preserving_impl', bi.limit_preserving_entails;
+      + apply limit_preserving_impl', bi.limit_preserving_emp_valid;
         solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
   Qed.
 
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index cd7f2a0a..949e0bcd 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -75,7 +75,7 @@ Section lft_contexts.
   Qed.
 
   Lemma llctx_elt_interp_acc_noend qmax x :
-    llctx_elt_interp qmax x -∗
+    llctx_elt_interp qmax x ⊢
     llctx_elt_interp_noend qmax x 1 ∗ (llctx_elt_interp_noend qmax x 1 -∗ llctx_elt_interp qmax x).
   Proof.
     destruct x as [κ κs].
@@ -106,7 +106,7 @@ Section lft_contexts.
   Proof. intros ???. by apply big_opL_permutation. Qed.
 
   Lemma llctx_interp_acc_noend qmax L :
-    llctx_interp qmax L -∗
+    llctx_interp qmax L ⊢
     llctx_interp_noend qmax L 1 ∗ (llctx_interp_noend qmax L 1 -∗ llctx_interp qmax L).
   Proof.
     rewrite /llctx_interp. setoid_rewrite llctx_elt_interp_acc_noend at 1.
@@ -145,7 +145,7 @@ Section lft_contexts.
   Context (E : elctx) (L : llctx).
 
   Definition lctx_lft_incl κ κ' : Prop :=
-    ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ ⌜κ ⊑ˢʸⁿ κ'⌝)%I.
+    ∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ ⌜κ ⊑ˢʸⁿ κ'⌝)%I.
 
   Definition lctx_lft_eq κ κ' : Prop :=
     lctx_lft_incl κ κ' ∧ lctx_lft_incl κ' κ.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 2339ac8d..bfbac4ea 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -49,7 +49,7 @@ Section arc.
   Qed.
 
   Lemma arc_persist_send tid tid' ν γ l ty `{!Send ty,!Sync ty} :
-    arc_persist tid ν γ l ty -∗ arc_persist tid' ν γ l ty.
+    arc_persist tid ν γ l ty ⊢ arc_persist tid' ν γ l ty.
   Proof.
     iIntros "#($ & ? & Hvs)". rewrite sync_change_tid. iFrame "#".
     iIntros "!> Hν". iMod ("Hvs" with "Hν") as "H". iModIntro. iNext.
@@ -174,7 +174,7 @@ Section arc.
   Proof. apply type_contractive_ne, _. Qed.
 
   Lemma arc_subtype ty1 ty2 :
-    type_incl ty1 ty2 -∗ type_incl (arc ty1) (arc ty2).
+    type_incl ty1 ty2 ⊢ type_incl (arc ty1) (arc ty2).
   Proof.
     iIntros "#Hincl". iPoseProof "Hincl" as "(#Hsz & #Hoincl & #Hsincl)".
     iSplit; first done. iSplit; iModIntro.
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index d793b11d..b9c67b55 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -148,7 +148,8 @@ Section code.
   Lemma mutex_acc E l ty tid q α κ :
     ↑lftN ⊆ E → ↑mutexN ⊆ E →
     let R := (&{κ}((l +ₗ 1) ↦∗: ty_own ty tid))%I in
-    lft_ctx -∗ &at{α,mutexN}(lock_proto l R) -∗ α ⊑ κ -∗
+    (* FIXME: using ⊢ to work around https://gitlab.mpi-sws.org/iris/iris/-/issues/496 *)
+    lft_ctx ⊢ &at{α,mutexN}(lock_proto l R) -∗ α ⊑ κ -∗
     □ ((q).[α] ={E,∅}=∗ ▷ lock_proto l R ∗ (▷ lock_proto l R ={∅,E}=∗ (q).[α])).
   Proof.
     (* FIXME: This should work: iIntros (?? R). *) intros ?? R.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index ba4af811..2409eef3 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -116,7 +116,7 @@ Section typing_rules.
   (* This lemma is helpful when switching from proving unsafe code in Iris
      back to proving it in the type system. *)
   Lemma type_type E L C T e :
-    typed_body E L C T e -∗ typed_body E L C T e.
+    typed_body E L C T e ⊢ typed_body E L C T e.
   Proof. done. Qed.
 
   (** This lemma can replace [κ1] by [κ2] and vice versa in positions that
diff --git a/theories/typing/sum.v b/theories/typing/sum.v
index c719d6f7..33b9953a 100644
--- a/theories/typing/sum.v
+++ b/theories/typing/sum.v
@@ -201,7 +201,7 @@ Section sum.
         - apply shr_locsE_subseteq. lia.
         - set_solver+. }
       destruct (Qp.lower_bound q'1 q'2) as (q' & q'01 & q'02 & -> & ->).
-      rewrite -(heap_mapsto_pred_op _ q' q'02); last (by intros; apply ty_size_eq).
+      rewrite -(heap_mapsto_pred_op _ q' q'02); last (by intros; iApply ty_size_eq).
       rewrite (fractional (Φ := λ q, _ ↦{q} _ ∗ _ ↦∗{q}: _)%I).
       iDestruct "HownC" as "[HownC1 HownC2]". iDestruct "Hown" as "[Hown1 Hown2]".
       iExists q'. iModIntro. iSplitL "Hown1 HownC1".
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 29154f26..366638aa 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -25,7 +25,7 @@ Record type `{!typeGS Σ} :=
 
     ty_shr_persistent κ tid l : Persistent (ty_shr κ tid l);
 
-    ty_size_eq tid vl : ty_own tid vl -∗ ⌜length vl = ty_size⌝;
+    ty_size_eq tid vl : ty_own tid vl ⊢ ⌜length vl = ty_size⌝;
     (* The mask for starting the sharing does /not/ include the
        namespace N, for allowing more flexibility for the user of
        this type (typically for the [own] type). AFAIK, there is no
@@ -114,7 +114,7 @@ Qed.
 
 Record simple_type `{!typeGS Σ} :=
   { st_own : thread_id → list val → iProp Σ;
-    st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
+    st_size_eq tid vl : st_own tid vl ⊢ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
 Global Instance: Params (@st_own) 2 := {}.
@@ -171,7 +171,7 @@ Section ofe.
     (lft -d> thread_id -d> loc -d> iPropO Σ).
   Let P (x : T) : Prop :=
     (∀ κ tid l, Persistent (x.2 κ tid l)) ∧
-    (∀ tid vl, x.1.2 tid vl -∗ ⌜length vl = x.1.1⌝) ∧
+    (∀ tid vl, x.1.2 tid vl ⊢ ⌜length vl = x.1.1⌝) ∧
     (∀ E κ l tid q, ↑lftN ⊆ E →
       lft_ctx -∗ &{κ} (l ↦∗: λ vs, x.1.2 tid vs) -∗
       q.[κ] ={E}=∗ x.2 κ tid l ∗ q.[κ]) ∧
@@ -216,9 +216,9 @@ Section ofe.
     - (* TODO: automate this *)
       repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
       + apply bi.limit_preserving_Persistent=> n ty1 ty2 Hty; apply Hty.
-      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; first by apply Hty. by rewrite Hty.
-      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
-      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+      + apply bi.limit_preserving_entails=> n ty1 ty2 Hty; last by rewrite Hty. apply Hty.
+      + apply bi.limit_preserving_emp_valid=> n ty1 ty2 Hty. repeat f_equiv; apply Hty.
+      + apply bi.limit_preserving_emp_valid=> n ty1 ty2 Hty. repeat f_equiv; apply Hty.
   Qed.
 
   Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=
@@ -410,7 +410,7 @@ Global Instance lst_copy_cons `{!typeGS Σ} ty tys :
   Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Send `{!typeGS Σ} (t : type) :=
-  send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
+  send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl ⊢ t.(ty_own) tid2 vl.
 Global Instance: Params (@Send) 2 := {}.
 
 Class ListSend `{!typeGS Σ} (tys : list type) := lst_send : Forall Send tys.
@@ -420,7 +420,7 @@ Global Instance lst_send_cons `{!typeGS Σ} ty tys :
   Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Sync `{!typeGS Σ} (t : type) :=
-  sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
+  sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l ⊢ t.(ty_shr) κ tid2 l.
 Global Instance: Params (@Sync) 2 := {}.
 
 Class ListSync `{!typeGS Σ} (tys : list type) := lst_sync : Forall Sync tys.
@@ -640,7 +640,7 @@ End iprop_subtyping.
 (** Prop-level conditional type inclusion/equality
     (may depend on assumptions in [E, L].) *)
 Definition subtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
-  ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
+  ∀ qmax qL, llctx_interp_noend qmax L qL ⊢ □ (elctx_interp E -∗ type_incl ty1 ty2).
 Global Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 88b326d1..e4b21bf4 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -150,7 +150,7 @@ Section type_context.
 
   (** Send typing contexts *)
   Class SendC (T : tctx) :=
-    sendc_change_tid tid1 tid2 : tctx_interp tid1 T -∗ tctx_interp tid2 T.
+    sendc_change_tid tid1 tid2 : tctx_interp tid1 T ⊢ tctx_interp tid2 T.
 
   Global Instance tctx_nil_send : SendC [].
   Proof. done. Qed.
-- 
GitLab