From 93e0e17c56c60fe92d248a70ba13832a39dba474 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 May 2023 14:13:06 +0200
Subject: [PATCH] update dependencies

---
 coq-reloc.opam                             |  2 +-
 theories/examples/folly_queue/refinement.v | 12 +++----
 theories/examples/folly_queue/ticketLock.v |  2 +-
 theories/examples/stack_helping/stack.v    |  4 +--
 theories/examples/various.v                |  2 +-
 theories/experimental/hocap/counter.v      |  4 +--
 theories/lib/polyeq.v                      |  2 +-
 theories/logic/adequacy.v                  |  2 +-
 theories/logic/rules.v                     | 40 ++++++++++++----------
 theories/logic/spec_ra.v                   |  4 +--
 theories/logic/spec_rules.v                | 20 ++++++-----
 theories/typing/interp.v                   |  8 ++---
 12 files changed, 53 insertions(+), 49 deletions(-)

diff --git a/coq-reloc.opam b/coq-reloc.opam
index 1c86cf8..6cb1918 100644
--- a/coq-reloc.opam
+++ b/coq-reloc.opam
@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2023-05-03.3.85295b18") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index 77be85f..fe1fd29 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -225,7 +225,7 @@ Section queue_refinement.
 
   Definition tokens_from γt n := own γt (set_above n).
   Definition token γt (n : nat) := own γt (set_singleton n).
-  Lemma tokens_take γ m : tokens_from γ m -∗ tokens_from γ (m + 1) ∗ token γ m.
+  Lemma tokens_take γ m : tokens_from γ m ⊢ tokens_from γ (m + 1) ∗ token γ m.
   Proof. rewrite /tokens_from /token -own_op comm -take_first. done. Qed.
 
   (* A single element queue contains: TS, location, gname for ghost state. *)
@@ -408,7 +408,7 @@ Section queue_refinement.
     0 < q →
     i < q →
     (popT `mod` q ≠ i) →
-    turn_ctx γ q i popT pushT -∗
+    turn_ctx γ q i popT pushT ⊢
     turn_ctx γ q i (popT + 1) pushT.
   Proof.
     iIntros (Hgt Hiq Hneq) "Hctx".
@@ -419,7 +419,7 @@ Section queue_refinement.
     0 < q →
     i < q →
     (pushT `mod` q ≠ i) →
-    turn_ctx γ q i popT pushT -∗
+    turn_ctx γ q i popT pushT ⊢
     turn_ctx γ q i popT (pushT+1).
   Proof.
     iIntros (Hgt Hiq Hneq) "Hctx".
@@ -428,7 +428,7 @@ Section queue_refinement.
 
   Lemma turn_ctx_incr_pop_eq γ q popT pushT :
     0 < q →
-    turn_ctx γ q (popT `mod` q) popT pushT -∗
+    turn_ctx γ q (popT `mod` q) popT pushT ⊢
     turn_ctx γ q (popT `mod` q) (popT + 1) pushT ∗
     dequeue_turn γ (popT `div` q).
   Proof.
@@ -444,7 +444,7 @@ Section queue_refinement.
 
   Lemma turn_ctx_incr_push_eq γ q popT pushT :
     0 < q →
-    turn_ctx γ q (pushT `mod` q) popT pushT -∗
+    turn_ctx γ q (pushT `mod` q) popT pushT ⊢
     turn_ctx γ q (pushT `mod` q) popT (pushT+1) ∗
     enqueue_turn γ (pushT `div` q).
   Proof.
@@ -678,7 +678,7 @@ Section queue_refinement.
     simpl.
     assert ({[n]} ∪ ∅ = {[n]}) as ->; first by set_solver.
     rewrite big_sepS_singleton.
-    done.
+    auto.
   Qed.
 
   Lemma enqueue_refinement (A : lrel Σ) (q : nat) γt γm γl ℓpop ℓpush ℓarr SEQs list l x x' :
diff --git a/theories/examples/folly_queue/ticketLock.v b/theories/examples/folly_queue/ticketLock.v
index 80e3676..92b56e0 100644
--- a/theories/examples/folly_queue/ticketLock.v
+++ b/theories/examples/folly_queue/ticketLock.v
@@ -54,7 +54,7 @@ Section contents.
     iApply "HΦ". rewrite /lock_inv. by iFrame "Hts Hinv".
   Qed.
 
-  Lemma turns_take γ m : turns_from γ m -∗ turns_from γ (m + 1) ∗ turn γ m.
+  Lemma turns_take γ m : turns_from γ m ⊢ turns_from γ (m + 1) ∗ turn γ m.
   Proof. by rewrite /turns_from /turn -own_op comm -take_first. Qed.
 
   Lemma acquire_spec γTS ts (turn : loc) :
diff --git a/theories/examples/stack_helping/stack.v b/theories/examples/stack_helping/stack.v
index e206268..b7a654e 100644
--- a/theories/examples/stack_helping/stack.v
+++ b/theories/examples/stack_helping/stack.v
@@ -224,13 +224,13 @@ Section sep_list2.
   Implicit Types Φ Ψ : nat → A → B → iProp Σ.
 
   Lemma big_sepL2_nil_inv_l Φ l2 :
-    ([∗ list] k↦y1;y2 ∈ []; l2, Φ k y1 y2) -∗ ⌜l2 = []⌝.
+    ([∗ list] k↦y1;y2 ∈ []; l2, Φ k y1 y2) ⊢ ⌜l2 = []⌝.
   Proof.
     rewrite big_sepL2_alt bi.and_elim_l /= -length_zero_iff_nil.
     by apply bi.pure_mono.
   Qed.
   Lemma big_sepL2_nil_inv_r Φ l1 :
-    ([∗ list] k↦y1;y2 ∈ l1; [], Φ k y1 y2) -∗ ⌜l1 = []⌝.
+    ([∗ list] k↦y1;y2 ∈ l1; [], Φ k y1 y2) ⊢ ⌜l1 = []⌝.
   Proof.
     rewrite big_sepL2_alt bi.and_elim_l /= length_zero_iff_nil.
     by apply bi.pure_mono.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index dcd92d4..a1737c3 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -47,7 +47,7 @@ Section proofs.
   Proof. by apply own_alloc. Qed.
   Lemma shoot γ `{oneshotG Σ} : pending γ ==∗ shot γ.
   Proof.
-    apply own_update.
+    apply bi.entails_wand, own_update.
     intros n [f |]; simpl; eauto.
     destruct f; simpl; try by inversion 1.
   Qed.
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index fed03f4..18c5e81 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -56,7 +56,7 @@ Section cnt_model.
       ==∗
       cnt_auth γ k ∗ cnt γ 1 k.
   Proof.
-    apply (bi.wand_intro_r (cnt_auth γ n)).
+    apply bi.entails_wand, (bi.wand_intro_r (cnt_auth γ n)).
     rewrite /cnt /cnt_auth - !own_op.
     apply own_update. apply auth_update, option_local_update.
     by apply exclusive_local_update.
@@ -76,7 +76,7 @@ Section cnt_model.
   Lemma cnt_agree_2 γ q n m :
     cnt_auth γ n -∗ cnt γ q m -∗ ⌜n = m⌝.
   Proof.
-    apply bi.wand_intro_r. rewrite /cnt /cnt_auth - !own_op.
+    apply bi.entails_wand, bi.wand_intro_r. rewrite /cnt /cnt_auth - !own_op.
     iIntros "H". iDestruct (own_valid with "H") as %Hfoo.
     iPureIntro; revert Hfoo.
     rewrite auth_both_valid_discrete.
diff --git a/theories/lib/polyeq.v b/theories/lib/polyeq.v
index 90ac134..4b444b9 100644
--- a/theories/lib/polyeq.v
+++ b/theories/lib/polyeq.v
@@ -31,7 +31,7 @@ Section proof.
 
   Lemma polyeq_true Ï„ v1 v2 :
     EqType τ →
-    interp τ [] v1 v2 -∗
+    interp τ [] v1 v2 ⊢
     REL polyeq Ï„ v1 v2 << #true : lrel_bool.
   Proof.
     intros HÏ„ ; revert v1 v2. induction HÏ„=> v1 v2 /=.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 664e046..c05ba0d 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -46,7 +46,7 @@ Proof.
       by rewrite /to_tpool /= insert_empty map_fmap_singleton //.
   - iIntros (v).
     iDestruct 1 as (v') "[Hj Hinterp]".
-    rewrite HA.
+    iDestruct (HA with "Hinterp") as "Hinterp".
     iDestruct "Hinterp" as %Hinterp.
     iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
     iDestruct "Hj" as "[#Hs Hj]".
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 4c942ea..2d32037 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -7,6 +7,8 @@ From iris.heap_lang Require Import proofmode.
 From reloc.logic Require Import model proofmode.spec_tactics.
 From reloc.prelude Require Import ctx_subst.
 
+Local Set Default Proof Using "Type".
+
 Section rules.
   Context `{relocG Σ}.
   Implicit Types A : lrel Σ.
@@ -121,7 +123,7 @@ Section rules.
   Lemma refines_newproph_r E K t A
     (Hmasked : nclose specN ⊆ E) :
     (∀ (p : proph_id), REL t << fill K (of_val #p) @ E : A)%I
-    -∗ REL t << fill K NewProph @ E : A.
+    ⊢ REL t << fill K NewProph @ E : A.
   Proof.
     iIntros "Hlog".
     iApply refines_step_r.
@@ -133,7 +135,7 @@ Section rules.
   Lemma refines_resolveproph_r E K t (p : proph_id) w A
     (Hmasked : nclose specN ⊆ E) :
     (REL t << fill K (of_val #()) @ E : A)%I
-    -∗ REL t << fill K (ResolveProph #p (of_val w)) @ E : A.
+    ⊢ REL t << fill K (ResolveProph #p (of_val w)) @ E : A.
   Proof.
     iIntros "Hlog".
     iApply refines_step_r.
@@ -145,7 +147,7 @@ Section rules.
   Lemma refines_store_r E K l e e' v v' A
     (Hmasked : nclose specN ⊆ E) :
     IntoVal e' v' →
-    l ↦ₛ v -∗
+    l ↦ₛ v ⊢
     (l ↦ₛ v' -∗ REL e << fill K (of_val #()) @ E : A) -∗
     REL e << fill K (#l <- e') @ E : A.
   Proof.
@@ -160,7 +162,7 @@ Section rules.
     (Hmasked : nclose specN ⊆ E) :
     IntoVal e v →
     (∀ l : loc, l ↦ₛ v -∗ REL t << fill K (of_val #l) @ E : A)%I
-    -∗ REL t << fill K (ref e) @ E : A.
+    ⊢ REL t << fill K (ref e) @ E : A.
   Proof.
     rewrite /IntoVal. intros <-.
     iIntros "Hlog".
@@ -172,7 +174,7 @@ Section rules.
 
   Lemma refines_load_r E K l q v t A
     (Hmasked : nclose specN ⊆ E) :
-    l ↦ₛ{q} v -∗
+    l ↦ₛ{q} v ⊢
     (l ↦ₛ{q} v -∗ REL t << fill K (of_val v) @ E : A)
     -∗ REL t << (fill K !#l) @ E : A.
   Proof.
@@ -186,7 +188,7 @@ Section rules.
   Lemma refines_xchg_r E K l e1 v1 v t A :
     nclose specN ⊆ E →
     IntoVal e1 v1 →
-    l ↦ₛ v -∗
+    l ↦ₛ v ⊢
     (l ↦ₛ v1 -∗ REL t << fill K (of_val v) @ E : A)
     -∗ REL t << fill K (Xchg #l e1) @ E : A.
   Proof.
@@ -203,7 +205,7 @@ Section rules.
     IntoVal e2 v2 →
     vals_compare_safe v v1 →
     v ≠ v1 →
-    l ↦ₛ v -∗
+    l ↦ₛ v ⊢
     (l ↦ₛ v -∗ REL t << fill K (of_val (v, #false)) @ E : A)
     -∗ REL t << fill K (CmpXchg #l e1 e2) @ E : A.
   Proof.
@@ -220,7 +222,7 @@ Section rules.
     IntoVal e2 v2 →
     vals_compare_safe v v1 →
     v = v1 →
-    l ↦ₛ v -∗
+    l ↦ₛ v ⊢
     (l ↦ₛ v2 -∗ REL t << fill K (of_val (v, #true)) @ E : A)
     -∗ REL t << fill K (CmpXchg #l e1 e2) @ E : A.
   Proof.
@@ -248,7 +250,7 @@ Section rules.
   Lemma refines_fork_r E K (e t : expr) A
    (Hmasked : nclose specN ⊆ E) :
    (∀ k, refines_right k e -∗
-     REL t << fill K (of_val #()) @ E : A) -∗
+     REL t << fill K (of_val #()) @ E : A) ⊢
    REL t << fill K (Fork e) @ E : A.
   Proof.
     iIntros "Hlog".
@@ -294,7 +296,7 @@ Section rules.
 
   Lemma refines_fork_l K E e t A :
    (|={⊤,E}=> ▷ (WP e {{ _, True }} ∗
-    (REL fill K (of_val #()) << t @ E : A))) -∗
+    (REL fill K (of_val #()) << t @ E : A))) ⊢
    REL fill K (Fork e) << t : A.
   Proof.
     iIntros "Hlog".
@@ -307,7 +309,7 @@ Section rules.
     IntoVal e v →
     (|={⊤,E}=> ▷ (∀ l : loc, l ↦ v -∗
            REL fill K (of_val #l) << t @ E : A))%I
-    -∗ REL fill K (ref e) << t : A.
+    ⊢ REL fill K (ref e) << t : A.
   Proof.
     iIntros (<-) "Hlog".
     iApply refines_atomic_l; auto.
@@ -319,7 +321,7 @@ Section rules.
     (|={⊤,E}=> ▷ (∀ (vs : list (val*val)) (p : proph_id),
            proph p vs -∗
            REL fill K (of_val #p) << t @ E : A))%I
-    -∗ REL fill K NewProph << t : A.
+    ⊢ REL fill K NewProph << t : A.
   Proof.
     iIntros "Hlog".
     iApply refines_atomic_l; auto.
@@ -333,7 +335,7 @@ Section rules.
            ▷ (∀ (vs' : list (val*val)), ⌜vs = (LitV LitUnit,w)::vs'⌝ -∗
                   proph p vs' -∗
                   REL fill K (of_val #()) << t @ E : A))%I
-    -∗ REL fill K (ResolveProph #p w) << t : A.
+    ⊢ REL fill K (ResolveProph #p w) << t : A.
   Proof.
     iIntros "Hlog".
     iApply refines_atomic_l; auto.
@@ -350,7 +352,7 @@ Section rules.
            WP e @ E {{ v, ∀ (vs' : list (val*val)), ⌜vs = (v,w)::vs'⌝ -∗
                   proph p vs' -∗
                   REL fill K (of_val v) << t @ E : A }})%I
-    -∗ REL fill K (Resolve e #p w) << t : A.
+    ⊢ REL fill K (Resolve e #p w) << t : A.
   Proof.
     iIntros (??) "Hlog".
     iApply refines_atomic_l; auto.
@@ -363,7 +365,7 @@ Section rules.
     (|={⊤,E}=> ∃ v',
       ▷(l ↦{q} v') ∗
       ▷(l ↦{q} v' -∗ (REL fill K (of_val v') << t @ E : A)))%I
-    -∗ REL fill K (! #l) << t : A.
+    ⊢ REL fill K (! #l) << t : A.
   Proof.
     iIntros "Hlog".
     iApply refines_atomic_l; auto.
@@ -375,7 +377,7 @@ Section rules.
     IntoVal e v' →
     (|={⊤,E}=> ∃ v, ▷ l ↦ v ∗
       ▷(l ↦ v' -∗ REL fill K (of_val #()) << t @ E : A))
-    -∗ REL fill K (#l <- e) << t : A.
+    ⊢ REL fill K (#l <- e) << t : A.
   Proof.
     iIntros (<-) "Hlog".
     iApply refines_atomic_l; auto.
@@ -387,7 +389,7 @@ Section rules.
     IntoVal e v' →
     (|={⊤,E}=> ∃ v, ▷ l ↦ v ∗
       ▷(l ↦ v' -∗ REL fill K (of_val v) << t @ E : A))
-    -∗ REL fill K (Xchg #l e) << t : A.
+    ⊢ REL fill K (Xchg #l e) << t : A.
   Proof.
     iIntros (<-) "Hlog".
     iApply refines_atomic_l; auto.
@@ -402,7 +404,7 @@ Section rules.
     (|={⊤,E}=> ∃ v', ▷ l ↦ v' ∗
      (⌜v' ≠ v1⌝ -∗ ▷ (l ↦ v' -∗ REL fill K (of_val (v', #false)) << t @ E : A)) ∧
      (⌜v' = v1⌝ -∗ ▷ (l ↦ v2 -∗ REL fill K (of_val (v', #true)) << t @ E : A)))
-    -∗ REL fill K (CmpXchg #l e1 e2) << t : A.
+    ⊢ REL fill K (CmpXchg #l e1 e2) << t : A.
   Proof.
     iIntros (<-<-?) "Hlog".
     iApply refines_atomic_l; auto.
@@ -424,7 +426,7 @@ Section rules.
     IntoVal e2 #i2 →
     (|={⊤,E}=> ∃ (i1 : Z), ▷ l ↦ #i1 ∗
      ▷ (l ↦ #(i1 + i2) -∗ REL fill K (of_val #i1) << t @ E : A))
-    -∗ REL fill K (FAA #l e2) << t : A.
+    ⊢ REL fill K (FAA #l e2) << t : A.
   Proof.
     iIntros (<-) "Hlog".
     iApply refines_atomic_l; auto.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index d5502dd..1ee22f3 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -167,7 +167,7 @@ Section mapsto.
 
   Lemma mapstoS_agree l q1 q2 v1 v2 : l ↦ₛ{q1} v1 -∗ l ↦ₛ{q2} v2 -∗ ⌜v1 = v2⌝.
   Proof.
-    apply bi.wand_intro_r.
+    apply bi.entails_wand, bi.wand_intro_r.
     rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
     f_equiv=> /=.
     rewrite -pair_op singleton_op right_id -pair_op.
@@ -180,7 +180,7 @@ Section mapsto.
   Lemma mapstoS_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
   Proof.
     rewrite heapS_mapsto_eq /heapS_mapsto_def own_valid !uPred.discrete_valid.
-    apply pure_mono=> /auth_frag_valid /= [_ Hfoo].
+    apply bi.entails_wand, pure_mono=> /auth_frag_valid /= [_ Hfoo].
     revert Hfoo. simpl. rewrite singleton_valid.
     by intros [? _].
   Qed.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 2bfb0ff..95a6751 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -6,6 +6,8 @@ From iris.heap_lang Require Export lang notation tactics.
 From reloc.logic Require Export spec_ra.
 Import uPred.
 
+Local Set Default Proof Using "Type".
+
 Section rules.
   Context `{relocG Σ}.
   Implicit Types P Q : iProp Σ.
@@ -44,7 +46,7 @@ Section rules.
     P →
     PureExec P n e e' →
     nclose specN ⊆ E →
-    spec_ctx ∗ j ⤇ fill K e ={E}=∗ spec_ctx ∗ j ⤇ fill K e'.
+    spec_ctx ∗ j ⤇ fill K e ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K e'.
   Proof.
     iIntros (HP Hex ?) "[#Hspec Hj]". iFrame "Hspec".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
@@ -132,7 +134,7 @@ Section rules.
   Lemma step_alloc E j K e v :
     IntoVal e v →
     nclose specN ⊆ E →
-    spec_ctx ∗ j ⤇ fill K (ref e) ={E}=∗ ∃ l, spec_ctx ∗ j ⤇ fill K (#l) ∗ l ↦ₛ v.
+    spec_ctx ∗ j ⤇ fill K (ref e) ⊢ |={E}=> ∃ l, spec_ctx ∗ j ⤇ fill K (#l) ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "[#Hinv Hj]". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
@@ -160,7 +162,7 @@ Section rules.
   Lemma step_load E j K l q v:
     nclose specN ⊆ E →
     spec_ctx ∗ j ⤇ fill K (!#l) ∗ l ↦ₛ{q} v
-    ={E}=∗ spec_ctx ∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
+    ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
   Proof.
     iIntros (?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
@@ -184,7 +186,7 @@ Section rules.
     IntoVal e v →
     nclose specN ⊆ E →
     spec_ctx ∗ j ⤇ fill K (#l <- e) ∗ l ↦ₛ v'
-    ={E}=∗ spec_ctx ∗ j ⤇ fill K #() ∗ l ↦ₛ v.
+    ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K #() ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
@@ -215,7 +217,7 @@ Section rules.
     IntoVal e v →
     nclose specN ⊆ E →
     spec_ctx ∗ j ⤇ fill K (Xchg #l e) ∗ l ↦ₛ v'
-    ={E}=∗ spec_ctx ∗ j ⤇ fill K (of_val v') ∗ l ↦ₛ v.
+    ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (of_val v') ∗ l ↦ₛ v.
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
@@ -250,7 +252,7 @@ Section rules.
     vals_compare_safe v' v1 →
     v' ≠ v1 →
     spec_ctx ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ{q} v'
-    ={E}=∗ spec_ctx ∗ j ⤇ fill K (v', #false)%V ∗ l ↦ₛ{q} v'.
+    ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (v', #false)%V ∗ l ↦ₛ{q} v'.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)". iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
@@ -277,7 +279,7 @@ Section rules.
     vals_compare_safe v1' v1 →
     v1' = v1 →
     spec_ctx ∗ j ⤇ fill K (CmpXchg #l e1 e2) ∗ l ↦ₛ v1'
-    ={E}=∗ spec_ctx ∗ j ⤇ fill K (v1', #true)%V ∗ l ↦ₛ v2.
+    ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K (v1', #true)%V ∗ l ↦ₛ v2.
   Proof.
     iIntros (<-<-???) "(#Hinv & Hj & Hl)"; subst. iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
@@ -308,7 +310,7 @@ Section rules.
     IntoVal e1 #i2 →
     nclose specN ⊆ E →
     spec_ctx ∗ j ⤇ fill K (FAA #l e1) ∗ l ↦ₛ #i1
-    ={E}=∗ spec_ctx ∗ j ⤇ fill K #i1 ∗ l ↦ₛ #(i1+i2).
+    ⊢ |={E}=> spec_ctx ∗ j ⤇ fill K #i1 ∗ l ↦ₛ #(i1+i2).
   Proof.
     iIntros (<-?) "(#Hinv & Hj & Hl)"; subst. iFrame "Hinv".
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
@@ -337,7 +339,7 @@ Section rules.
   (** Fork *)
   Lemma step_fork E j K e :
     nclose specN ⊆ E →
-    spec_ctx ∗ j ⤇ fill K (Fork e) ={E}=∗
+    spec_ctx ∗ j ⤇ fill K (Fork e) ⊢ |={E}=>
     ∃ j', (spec_ctx ∗ j ⤇ fill K #()) ∗ (spec_ctx ∗ j' ⤇ e).
   Proof.
     iIntros (?) "[#Hspec Hj]". iFrame "Hspec".
diff --git a/theories/typing/interp.v b/theories/typing/interp.v
index 6d41cb4..ff03613 100644
--- a/theories/typing/interp.v
+++ b/theories/typing/interp.v
@@ -48,7 +48,7 @@ Section semtypes.
 
   Lemma unboxed_type_sound τ Δ v v' :
     UnboxedType τ →
-    interp τ Δ v v' -∗ ⌜val_is_unboxed v ∧ val_is_unboxed v'⌝.
+    interp τ Δ v v' ⊢ ⌜val_is_unboxed v ∧ val_is_unboxed v'⌝.
   Proof.
     induction 1; simpl;
     first [iDestruct 1 as (? ?) "[% [% ?]]"
@@ -59,7 +59,7 @@ Section semtypes.
 
   Lemma eq_type_sound τ Δ v v' :
     EqType τ →
-    interp τ Δ v v' -∗ ⌜v = v'⌝.
+    interp τ Δ v v' ⊢ ⌜v = v'⌝.
   Proof.
     intros HÏ„; revert v v'; induction HÏ„; iIntros (v v') "#H1 /=".
     - by iDestruct "H1" as %[-> ->].
@@ -224,7 +224,7 @@ Section env_typed.
 
   Lemma env_ltyped2_lookup Γ vs x A :
     Γ !! x = Some A →
-    ⟦ Γ ⟧* vs -∗ ∃ v1 v2, ⌜ vs !! x = Some (v1,v2) ⌝ ∧ A v1 v2.
+    ⟦ Γ ⟧* vs ⊢ ∃ v1 v2, ⌜ vs !! x = Some (v1,v2) ⌝ ∧ A v1 v2.
   Proof.
     intros ?. rewrite /env_ltyped2 big_sepM2_lookup_l //.
     iDestruct 1 as ([v1 v2] ?) "H". eauto with iFrame.
@@ -245,7 +245,7 @@ Section env_typed.
   Proof. apply (big_sepM2_empty' _). Qed.
 
   Lemma env_ltyped2_empty_inv vs :
-    ⟦ ∅ ⟧* vs -∗ ⌜vs = ∅⌝.
+    ⟦ ∅ ⟧* vs ⊢ ⌜vs = ∅⌝.
   Proof. apply big_sepM2_empty_r. Qed.
 
   Global Instance env_ltyped2_persistent Γ vs : Persistent (⟦ Γ ⟧* vs).
-- 
GitLab