From 3a4b14b934fbc750a3afc28e82bb867506db0f6a Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 7 Nov 2016 23:04:43 +0100
Subject: [PATCH] Merge current Iris trunk.

---
 iris                 |   2 +-
 theories/heap.v      | 167 +++++++++++++++++++++----------------------
 theories/lifetime.v  | 102 +++++++++++++-------------
 theories/lifting.v   |  60 ++++++++--------
 theories/memcpy.v    |   4 +-
 theories/perm.v      |  10 +--
 theories/perm_incl.v |  34 ++++-----
 theories/proofmode.v |  32 +++++----
 theories/type.v      |  76 ++++++++++----------
 theories/type_incl.v |  24 +++----
 theories/typing.v    | 110 ++++++++++++++--------------
 11 files changed, 310 insertions(+), 311 deletions(-)

diff --git a/iris b/iris
index bb5e21f2..5e3835f8 160000
--- a/iris
+++ b/iris
@@ -1 +1 @@
-Subproject commit bb5e21f21fd1b5be820005eb53750f84270ab4ec
+Subproject commit 5e3835f807768f42f77b6cc33bca039b8274a586
diff --git a/theories/heap.v b/theories/heap.v
index 9ce30f2f..97087b8f 100644
--- a/theories/heap.v
+++ b/theories/heap.v
@@ -47,7 +47,7 @@ Section definitions.
     proj2_sig heap_mapsto_aux.
 
   Definition heap_mapsto_vec (l : loc) (q : Qp) (vl : list val) : iProp Σ :=
-    ([★ list] i ↦ v ∈ vl, heap_mapsto (shift_loc l i) q v)%I.
+    ([∗ list] i ↦ v ∈ vl, heap_mapsto (shift_loc l i) q v)%I.
 
   Fixpoint inter (i0 : Z) (n : nat) : gmapR Z (exclR unitC) :=
     match n with O => ∅ | S n => <[i0 := Excl ()]>(inter (i0+1) n) end.
@@ -60,9 +60,9 @@ Section definitions.
     proj2_sig heap_freeable_aux.
 
   Definition heap_inv : iProp Σ :=
-    (∃ (σ:state) hF, ownP σ ★ own heap_name (● to_heap σ)
-                            ★ own heap_freeable_name (● hF)
-                            ★ ■ heap_freeable_rel σ hF)%I.
+    (∃ (σ:state) hF, ownP σ ∗ own heap_name (● to_heap σ)
+                            ∗ own heap_freeable_name (● hF)
+                            ∗ ■ heap_freeable_rel σ hF)%I.
   Definition heap_ctx : iProp Σ := inv heapN heap_inv.
 
   Global Instance heap_ctx_persistent : PersistentP heap_ctx.
@@ -78,14 +78,14 @@ Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : uPred_scope.
 Notation "l ↦ v" := (heap_mapsto l 1 v) (at level 20) : uPred_scope.
 
-Notation "l ↦★{ q } vl" := (heap_mapsto_vec l q vl)
-  (at level 20, q at level 50, format "l  ↦★{ q }  vl") : uPred_scope.
-Notation "l ↦★ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : uPred_scope.
+Notation "l ↦∗{ q } vl" := (heap_mapsto_vec l q vl)
+  (at level 20, q at level 50, format "l  ↦∗{ q }  vl") : uPred_scope.
+Notation "l ↦∗ vl" := (heap_mapsto_vec l 1 vl) (at level 20) : uPred_scope.
 
-Notation "l ↦★{ q }: P" := (∃ vl, l ↦★{ q } vl ★ P vl)%I
-  (at level 20, q at level 50, format "l  ↦★{ q }:  P") : uPred_scope.
-Notation "l ↦★: P " := (∃ vl, l ↦★ vl ★ P vl)%I
-  (at level 20, format "l  ↦★:  P") : uPred_scope.
+Notation "l ↦∗{ q }: P" := (∃ vl, l ↦∗{ q } vl ∗ P vl)%I
+  (at level 20, q at level 50, format "l  ↦∗{ q }:  P") : uPred_scope.
+Notation "l ↦∗: P " := (∃ vl, l ↦∗ vl ∗ P vl)%I
+  (at level 20, format "l  ↦∗:  P") : uPred_scope.
 
 Notation "†{ q } l … n" := (heap_freeable l q n)
   (at level 20, q at level 50, format "†{ q } l … n") : uPred_scope.
@@ -117,19 +117,19 @@ Section heap.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l↦{q}v).
   Proof. rewrite heap_mapsto_eq /heap_mapsto_def. apply _. Qed.
 
-  Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦★{q} vl).
+  Global Instance heap_mapsto_vec_timeless l q vl : TimelessP (l ↦∗{q} vl).
   Proof. apply _. Qed.
 
   Global Instance heap_freeable_timeless q l n : TimelessP (†{q}l…n).
   Proof. rewrite heap_freeable_eq /heap_freeable_def. apply _. Qed.
 
-  Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ★ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
+  Lemma heap_mapsto_op_eq l q1 q2 v : l ↦{q1} v ∗ l ↦{q2} v ⊣⊢ l ↦{q1+q2} v.
   Proof.
     by rewrite heap_mapsto_eq -own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
   Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
-    l ↦{q1} v1 ★ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
+    l ↦{q1} v1 ∗ l ↦{q2} v2 ⊣⊢ v1 = v2 ∧ l ↦{q1+q2} v1.
   Proof.
     destruct (decide (v1 = v2)) as [->|].
     { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
@@ -139,34 +139,34 @@ Section heap.
     rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
   Qed.
 
-  Lemma heap_mapsto_vec_nil l q : l ↦★{q} [] ⊣⊢ True.
+  Lemma heap_mapsto_vec_nil l q : l ↦∗{q} [] ⊣⊢ True.
   Proof. by rewrite /heap_mapsto_vec big_sepL_nil. Qed.
 
   Lemma heap_mapsto_vec_app l q vl1 vl2 :
-    l ↦★{q} (vl1 ++ vl2) ⊣⊢ l ↦★{q} vl1 ★ shift_loc l (length vl1) ↦★{q} vl2.
+    l ↦∗{q} (vl1 ++ vl2) ⊣⊢ l ↦∗{q} vl1 ∗ shift_loc l (length vl1) ↦∗{q} vl2.
   Proof.
     rewrite /heap_mapsto_vec big_sepL_app.
     do 2 f_equiv. intros k v. by rewrite shift_loc_assoc_nat.
   Qed.
 
-  Lemma heap_mapsto_vec_singleton l q v : l ↦★{q} [v] ⊣⊢ l ↦{q} v.
+  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.
 
   Lemma heap_mapsto_vec_cons l q v vl:
-    l ↦★{q} (v :: vl) ⊣⊢ l ↦{q} v ★ shift_loc l 1 ↦★{q} vl.
+    l ↦∗{q} (v :: vl) ⊣⊢ l ↦{q} v ∗ shift_loc l 1 ↦∗{q} vl.
   Proof.
     by rewrite (heap_mapsto_vec_app l q [v] vl) heap_mapsto_vec_singleton.
   Qed.
 
   Lemma heap_mapsto_vec_op_eq l q1 q2 vl :
-    l ↦★{q1} vl ★ l ↦★{q2} vl ⊣⊢ l ↦★{q1+q2} vl.
+    l ↦∗{q1} vl ∗ l ↦∗{q2} vl ⊣⊢ l ↦∗{q1+q2} vl.
   Proof.
     rewrite /heap_mapsto_vec -big_sepL_sepL. by setoid_rewrite heap_mapsto_op_eq.
   Qed.
 
   Lemma heap_mapsto_vec_op l q1 q2 vl1 vl2 :
     length vl1 = length vl2 →
-    l ↦★{q1} vl1 ★ l ↦★{q2} vl2 ⊣⊢ vl1 = vl2 ∧ l ↦★{q1+q2} vl1.
+    l ↦∗{q1} vl1 ∗ l ↦∗{q2} vl2 ⊣⊢ vl1 = vl2 ∧ l ↦∗{q1+q2} vl1.
   Proof.
     iIntros (Hlen%Forall2_same_length); iSplit.
     - revert l. induction Hlen as [|v1 v2 vl1 vl2 _ _ IH]=> l.
@@ -179,7 +179,7 @@ Section heap.
 
   Lemma heap_mapsto_vec_prop_op l q1 q2 n (Φ : list val → iProp Σ) :
     (∀ vl, Φ vl ⊢ length vl = n) →
-    l ↦★{q1}: Φ ★ l ↦★{q2}: (λ vl, length vl = n) ⊣⊢ l ↦★{q1+q2}: Φ.
+    l ↦∗{q1}: Φ ∗ l ↦∗{q2}: (λ vl, length vl = n) ⊣⊢ l ↦∗{q1+q2}: Φ.
   Proof.
     intros Hlen. iSplit.
     - iIntros "[Hmt1 Hmt2]".
@@ -193,16 +193,16 @@ Section heap.
       iSplitL "Hmt1 Hown"; iExists _; by iFrame.
   Qed.
 
-  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ l ↦{q/2} v ★ l ↦{q/2} v.
+  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ l ↦{q/2} v ∗ l ↦{q/2} v.
   Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
 
   Lemma heap_mapsto_vec_op_split l q vl :
-    l ↦★{q} vl ⊣⊢ l ↦★{q/2} vl ★ l ↦★{q/2} vl.
+    l ↦∗{q} vl ⊣⊢ l ↦∗{q/2} vl ∗ l ↦∗{q/2} vl.
   Proof. by rewrite heap_mapsto_vec_op_eq Qp_div_2. Qed.
 
   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 (◯ [⋅ list] i ↦ v ∈ vl,
       {[shift_loc l i := (q, Cinr 0%nat, DecAgree v)]}).
   Proof.
     rewrite /heap_mapsto_vec heap_mapsto_eq /heap_mapsto_def /heap_mapsto_st=>?.
@@ -233,7 +233,7 @@ Section heap.
   Proof. revert i. induction n as [|n IH]=>i. done. by apply insert_valid. Qed.
 
   Lemma heap_freeable_op_eq l q1 q2 n n' :
-    †{q1}l…n ★ †{q2}shift_loc l n…n' ⊣⊢ †{q1+q2}l…(n+n').
+    †{q1}l…n ∗ †{q2}shift_loc l n…n' ⊣⊢ †{q1+q2}l…(n+n').
   Proof.
     by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
       op_singleton pair_op inter_op.
@@ -305,8 +305,8 @@ Section heap.
   Lemma heap_alloc_vs σ l vl:
     (∀ 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 (● to_heap (init_mem l vl σ))
+       ∗ own heap_name (◯ [⋅ list] i ↦ v ∈ vl,
            {[shift_loc l i := (1%Qp, Cinr 0%nat, DecAgree v)]}).
   Proof.
     intros FREE. rewrite -own_op. apply own_update, auth_update_alloc.
@@ -325,12 +325,12 @@ Section heap.
   Lemma wp_alloc E n :
     nclose heapN ⊆ E → 0 < n →
     {{{ heap_ctx }}} Alloc (Lit $ LitInt n) @ E
-    {{{ l vl; LitV $ LitLoc l, n = length vl ★ †l…(Z.to_nat n) ★ l ↦★ vl }}}.
+    {{{ l vl, RET LitV $ LitLoc l; n = length vl ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
   Proof.
-    iIntros (???) "[#Hinv HΦ]". rewrite /heap_ctx /heap_inv.
+    iIntros (???) "#Hinv HΦ". rewrite /heap_ctx /heap_inv.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
-    iApply wp_alloc_pst=> //. iNext.
-    iIntros "{$Hσ}". iIntros (l σ') "(% & #Hσσ' & Hσ')".
+    iApply (wp_alloc_pst with "[$Hσ]")=> //.
+    iNext. iIntros (l σ') "(% & #Hσσ' & Hσ')".
     iDestruct "Hσσ'" as %(vl & HvlLen & Hvl).
     assert (vl ≠ []) by (intros ->; simpl in *; lia).
     iMod (heap_alloc_vs with "[$Hvalσ]") as "[Hvalσ' Hmapsto]"; first done.
@@ -347,9 +347,9 @@ 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 (◯ [⋅ list] i ↦ v ∈ vl,
       {[shift_loc l i := (1%Qp, Cinr 0%nat, DecAgree v)]})
-    ==★ own heap_name (● to_heap (free_mem l (length vl) σ)).
+    ==∗ own heap_name (● to_heap (free_mem l (length vl) σ)).
   Proof.
     rewrite -own_op. apply own_update, auth_update_dealloc.
     revert σ l. induction vl as [|v vl IH]=> σ l; [done|].
@@ -370,11 +370,11 @@ Section heap.
   Lemma wp_free E (n:Z) l vl :
     nclose heapN ⊆ E →
     n = length vl →
-    {{{ heap_ctx ★ ▷ l ↦★ vl ★ ▷ †l…(length vl) }}}
+    {{{ heap_ctx ∗ ▷ l ↦∗ vl ∗ ▷ †l…(length vl) }}}
       Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
-    {{{ ; LitV LitUnit, True }}}.
+    {{{ RET LitV LitUnit; True }}}.
   Proof.
-    iIntros (???Φ) "[(#Hinv & >Hmt & >Hf) HΦ]". rewrite /heap_ctx /heap_inv.
+    iIntros (???Φ) "(#Hinv & >Hmt & >Hf) HΦ". rewrite /heap_ctx /heap_inv.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & REL)" "Hclose". iDestruct "REL" as %REL.
     rewrite heap_freeable_eq /heap_freeable_def.
     iDestruct (own_valid_2 with "[$HhF $Hf]") as % [Hl Hv]%auth_valid_discrete_2.
@@ -384,9 +384,9 @@ Section heap.
     assert (vl ≠ []).
     { intros ->. by destruct (REL (l.1) (1%Qp, ∅)) as [[] ?]. }
     assert (0 < n) by (subst n; by destruct vl).
-    iApply (wp_free_pst _ σ); auto.
+    iApply (wp_free_pst _ σ with "[$Hσ]"). by auto.
     { intros i. subst n. eauto using heap_freeable_is_Some. }
-    iNext. iIntros "{$Hσ} Hσ". iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
+    iNext. iIntros "Hσ". iMod (heap_free_vs with "[Hmt Hvalσ]") as "Hvalσ".
     { rewrite heap_mapsto_vec_combine //. iFrame. }
     iMod (own_update_2 with "[$HhF $Hf]") as "HhF".
     { apply auth_update_dealloc, (delete_singleton_local_update _ _ _). }
@@ -396,7 +396,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_lookup l ls q v σ:
-    own heap_name (● to_heap σ) ★
+    own heap_name (● to_heap σ) ∗
     own heap_name (â—¯ {[ l := (q, to_lock_stateR ls, DecAgree v) ]})
     ⊢ ■ ∃ n' : nat,
         σ !! l = Some (match ls with RSt n => RSt (n+n') | WSt => WSt end, v).
@@ -413,7 +413,7 @@ Section heap.
   Qed.
 
   Lemma heap_mapsto_lookup_1 l ls v σ:
-    own heap_name (● to_heap σ) ★
+    own heap_name (● to_heap σ) ∗
     own heap_name (â—¯ {[ l := (1%Qp, to_lock_stateR ls, DecAgree v) ]})
     ⊢ ■ (σ !! l = Some (ls, v)).
   Proof.
@@ -428,23 +428,23 @@ Section heap.
 
   Lemma wp_read_sc E l q v :
     nclose heapN ⊆ E →
-    {{{ heap_ctx ★ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
-    {{{; v, l ↦{q} v }}}.
+    {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read ScOrd (Lit $ LitLoc l) @ E
+    {{{ RET v; l ↦{q} v }}}.
   Proof.
-    iIntros (??) "[[#Hinv >Hv] HΦ]".
+    iIntros (??) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iApply wp_read_sc_pst; first done. iNext. iIntros "{$Hσ} Hσ".
+    iApply (wp_read_sc_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
     iNext. iExists σ, hF. iFrame. eauto.
   Qed.
 
   Lemma heap_read_vs σ n1 n2 nf l q v:
     σ !! l = Some (RSt (n1 + nf), v) →
-    own heap_name (● to_heap σ) ★ heap_mapsto_st (RSt n1) l q v
-    ==★ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
-        ★ heap_mapsto_st (RSt n2) l q v.
+    own heap_name (● to_heap σ) ∗ heap_mapsto_st (RSt n1) l q v
+    ==∗ own heap_name (● to_heap (<[l:=(RSt (n2 + nf), v)]> σ))
+        ∗ heap_mapsto_st (RSt n2) l q v.
   Proof.
     intros Hσv. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
@@ -455,10 +455,10 @@ Section heap.
 
   Lemma wp_read_na E l q v :
     nclose heapN ⊆ E →
-    {{{ heap_ctx ★ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
-    {{{; v, l ↦{q} v }}}.
+    {{{ heap_ctx ∗ ▷ l ↦{q} v }}} Read Na1Ord (Lit $ LitLoc l) @ E
+    {{{ RET v; l ↦{q} v }}}.
   Proof.
-    iIntros (??Φ) "[[#Hinv >Hv] HΦ]".
+    iIntros (??Φ) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iApply (wp_read_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
@@ -471,7 +471,7 @@ Section heap.
     iModIntro. clear dependent n σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iApply wp_read_na2_pst; first done. iNext. iIntros "{$Hσ} Hσ".
+    iApply (wp_read_na2_pst with "[$Hσ]"); first done. iNext. iIntros "Hσ".
     iMod (heap_read_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
@@ -479,9 +479,9 @@ Section heap.
 
   Lemma heap_write_vs σ st1 st2 l v v':
     σ !! l = Some (st1, v) →
-    own heap_name (● to_heap σ) ★ heap_mapsto_st st1 l 1%Qp v
-    ==★ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
-        ★ heap_mapsto_st st2 l 1%Qp v'.
+    own heap_name (● to_heap σ) ∗ heap_mapsto_st st1 l 1%Qp v
+    ==∗ own heap_name (● to_heap (<[l:=(st2, v')]> σ))
+        ∗ heap_mapsto_st st2 l 1%Qp v'.
   Proof.
     intros Hσv. rewrite -!own_op to_heap_insert.
     eapply own_update, auth_update, singleton_local_update.
@@ -491,14 +491,14 @@ Section heap.
 
   Lemma wp_write_sc E l e v v' :
     nclose heapN ⊆ E → to_val e = Some v →
-    {{{ heap_ctx ★ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
-    {{{; LitV LitUnit, l ↦ v }}}.
+    {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write ScOrd (Lit $ LitLoc l) e @ E
+    {{{ RET LitV LitUnit; l ↦ v }}}.
   Proof.
-    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
+    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_write_sc_pst; [done|]. iNext. iIntros "{$Hσ} Hσ".
+    iApply (wp_write_sc_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
@@ -506,10 +506,10 @@ Section heap.
 
   Lemma wp_write_na E l e v v' :
     nclose heapN ⊆ E → to_val e = Some v →
-    {{{ heap_ctx ★ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
-    {{{; LitV LitUnit, l ↦ v }}}.
+    {{{ heap_ctx ∗ ▷ l ↦ v' }}} Write Na1Ord (Lit $ LitLoc l) e @ E
+    {{{ RET LitV LitUnit; l ↦ v }}}.
   Proof.
-    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
+    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iApply (wp_write_na1_pst E).
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
@@ -522,7 +522,7 @@ Section heap.
     iModIntro. clear dependent σ hF.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_write_na2_pst; [done|]. iNext. iIntros "{$Hσ} Hσ".
+    iApply (wp_write_na2_pst with "[$Hσ]"); [done|]. iNext. iIntros "Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
@@ -530,54 +530,53 @@ Section heap.
 
   Lemma wp_cas_int_fail E l q z1 e2 v2 zl :
     nclose heapN ⊆ E → to_val e2 = Some v2 → z1 ≠ zl →
-    {{{ heap_ctx ★ ▷ l ↦{q} (LitV $ LitInt zl) }}}
+    {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitInt zl) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
-    {{{;LitV $ LitInt 0, l ↦{q} (LitV $ LitInt zl) }}}.
+    {{{ RET LitV $ LitInt 0; l ↦{q} (LitV $ LitInt zl) }}}.
   Proof.
-    iIntros (? <-%of_to_val ??) "[[#Hinv >Hv] HΦ]".
+    iIntros (? <-%of_to_val ??) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hv]") as %[n Hσl].
-    iApply wp_cas_fail_pst; eauto.
+    iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_false. }
-    iNext. iIntros "{$Hσ} Hσ".
-    iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
+    iNext. iIntros "Hσ". iMod ("Hclose" with "[-Hv HΦ]") as "_"; last by iApply "HΦ".
     iNext. iExists _, hF. iFrame. eauto using heap_freeable_rel_stable.
   Qed.
 
   Lemma wp_cas_loc_fail E l q q' q1 l1 v1' e2 v2 l' vl' :
     nclose heapN ⊆ E → to_val e2 = Some v2 → l1 ≠ l' →
-    {{{ heap_ctx ★ ▷ l ↦{q} (LitV $ LitLoc l') ★ ▷ l' ↦{q'} vl' ★ ▷ l1 ↦{q1} v1' }}}
+    {{{ heap_ctx ∗ ▷ l ↦{q} (LitV $ LitLoc l') ∗ ▷ l' ↦{q'} vl' ∗ ▷ l1 ↦{q1} v1' }}}
       CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
-    {{{;LitV $ LitInt 0,
-        l ↦{q} (LitV $ LitLoc l') ★ l' ↦{q'} vl' ★ l1 ↦{q1} v1' }}}.
+    {{{ RET LitV $ LitInt 0;
+        l ↦{q} (LitV $ LitLoc l') ∗ l' ↦{q'} vl' ∗ l1 ↦{q1} v1' }}}.
   Proof.
-    iIntros (? <-%of_to_val ??) "[(#Hinv & >Hl & >Hl' & >Hl1) HΦ]".
+    iIntros (? <-%of_to_val ??) "(#Hinv & >Hl & >Hl' & >Hl1) HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl]") as %[n Hσl].
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl']") as %[n' Hσl'].
     iDestruct (heap_mapsto_lookup with "[$Hvalσ $Hl1]") as %[n1 Hσl1].
-    iApply wp_cas_fail_pst; eauto.
+    iApply (wp_cas_fail_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_false // Hσl1 Hσl'. }
-    iNext. iIntros "{$Hσ} Hσ ".
+    iNext. iIntros "Hσ ".
     iMod ("Hclose" with "[-Hl Hl' Hl1 HΦ]") as "_"; last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. by iFrame.
   Qed.
 
   Lemma wp_cas_int_suc E l z1 e2 v2 :
     nclose heapN ⊆ E → to_val e2 = Some v2 →
-    {{{ heap_ctx ★ ▷ l ↦ (LitV $ LitInt z1) }}}
+    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitInt z1) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitInt z1) e2 @ E
-    {{{; LitV $ LitInt 1, l ↦ v2 }}}.
+    {{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
   Proof.
-    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
+    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_cas_suc_pst; eauto.
+    iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_true. }
-    iNext. iIntros "{$Hσ} Hσ".
+    iNext. iIntros "Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
@@ -585,17 +584,17 @@ Section heap.
 
   Lemma wp_cas_loc_suc E l l1 e2 v2 :
     nclose heapN ⊆ E → to_val e2 = Some v2 →
-    {{{ heap_ctx ★ ▷ l ↦ (LitV $ LitLoc l1) }}}
+    {{{ heap_ctx ∗ ▷ l ↦ (LitV $ LitLoc l1) }}}
       CAS (Lit $ LitLoc l) (Lit $ LitLoc l1) e2 @ E
-    {{{; LitV $ LitInt 1, l ↦ v2 }}}.
+    {{{ RET LitV $ LitInt 1; l ↦ v2 }}}.
   Proof.
-    iIntros (? <-%of_to_val?) "[[#Hinv >Hv] HΦ]".
+    iIntros (? <-%of_to_val?) "[#Hinv >Hv] HΦ".
     rewrite /heap_ctx /heap_inv heap_mapsto_eq /heap_mapsto_def.
     iInv heapN as (σ hF) ">(Hσ & Hvalσ & HhF & %)" "Hclose".
     iDestruct (heap_mapsto_lookup_1 with "[$Hvalσ $Hv]") as %?.
-    iApply wp_cas_suc_pst; eauto.
+    iApply (wp_cas_suc_pst with "[$Hσ]"); eauto.
     { by rewrite /= bool_decide_true. }
-    iNext. iIntros "{$Hσ} Hσ".
+    iNext. iIntros "Hσ".
     iMod (heap_write_vs with "[$Hvalσ $Hv]") as "[Hvalσ Hv]"; first done.
     iMod ("Hclose" with "[-Hv HΦ]"); last by iApply "HΦ"; iFrame.
     iNext. iExists _, hF. iFrame. eauto using  heap_freeable_rel_stable.
diff --git a/theories/lifetime.v b/theories/lifetime.v
index 16b743b6..6bb618a1 100644
--- a/theories/lifetime.v
+++ b/theories/lifetime.v
@@ -38,7 +38,7 @@ Section defs.
     own toks_name (◯ (Cinl <$> omap (Qp_nat_mul q) κ)).
 
   Definition lft_dead (κ : lifetime) : iProp Σ :=
-    (∃ Λ, ■ (∃ n, κ !! Λ = Some (S n)) ★
+    (∃ Λ, ■ (∃ n, κ !! Λ = Some (S n)) ∗
             own toks_name (◯ {[ Λ := Cinr () ]}))%I.
 
 End defs.
@@ -53,7 +53,7 @@ Parameter lft_idx_borrow_persist: ∀ `{lifetimeG Σ} (i : gname), iProp Σ.
 Parameter lft_idx_borrow_own : ∀ `{lifetimeG Σ} (i : gname), iProp Σ.
 
 Definition lft_borrow `{lifetimeG Σ} (κ : lifetime) (P : iProp Σ) : iProp Σ :=
-  (∃ i, lft_idx_borrow κ i P ★ lft_idx_borrow_own i)%I.
+  (∃ i, lft_idx_borrow κ i P ∗ lft_idx_borrow_own i)%I.
 
 (*** Notations  *)
 
@@ -104,7 +104,7 @@ Section lft.
   Proof. solve_proper. Qed.
 
   (** Basic rules about lifetimes  *)
-  Lemma lft_own_op q κ1 κ2 : q.[κ1] ★ q.[κ2] ⊣⊢ q.[κ1 ⋅ κ2].
+  Lemma lft_own_op q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⋅ κ2].
   Proof.
     rewrite /lft_own -own_op. f_equiv. constructor. done. move=>Λ /=.
     rewrite lookup_op !lookup_fmap !lookup_omap lookup_op.
@@ -126,7 +126,7 @@ Section lft.
   Qed.
 
   Lemma lft_own_frac_op κ q q':
-       (q + q').[κ] ⊣⊢ q.[κ] ★ q'.[κ].
+       (q + q').[κ] ⊣⊢ q.[κ] ∗ q'.[κ].
   Proof.
     rewrite /lft_own -own_op -auth_frag_op. f_equiv. constructor. done. simpl.
     intros Λ. rewrite lookup_op !lookup_fmap !lookup_omap. apply reflexive_eq.
@@ -138,33 +138,33 @@ Section lft.
 
   (* FIXME : merging begin and end. *)
   Axiom lft_create :
-    ∀ `(nclose lftN ⊆ E), True ={E}=★ ∃ κ, 1.[κ] ★ □ (1.[κ] ={⊤,∅}▷=★ [†κ]).
+    ∀ `(nclose lftN ⊆ E), True ={E}=∗ ∃ κ, 1.[κ] ∗ □ (1.[κ] ={⊤,∅}▷=∗ [†κ]).
 
   Axiom lft_idx_borrow_persist_upd :
-    ∀ `(nclose lftN ⊆ E) i, lft_idx_borrow_own i ={E}=★ lft_idx_borrow_persist i.
+    ∀ `(nclose lftN ⊆ E) i, lft_idx_borrow_own i ={E}=∗ lft_idx_borrow_persist i.
   Axiom lft_idx_borrow_own_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,
-      lft_idx_borrow κ i P ⊢ lft_idx_borrow_own i ★ q.[κ] ={E}=★ ▷ P ★
-                                 (▷ P ={E}=★ lft_idx_borrow_own i ★ q.[κ]).
+      lft_idx_borrow κ i P ⊢ lft_idx_borrow_own i ∗ q.[κ] ={E}=∗ ▷ P ∗
+                                 (▷ P ={E}=∗ lft_idx_borrow_own i ∗ q.[κ]).
   Axiom lft_idx_borrow_persist_acc :
     ∀ `(nclose lftN ⊆ E) q κ i P,
-      lft_idx_borrow κ i P ⊢ lft_idx_borrow_persist i -★
-            q.[κ] ={E,E∖lftN}=★ ▷ P ★ (▷ P ={E∖lftN,E}=★ q.[κ]).
+      lft_idx_borrow κ i P ⊢ lft_idx_borrow_persist i -∗
+            q.[κ] ={E,E∖lftN}=∗ ▷ P ∗ (▷ P ={E∖lftN,E}=∗ q.[κ]).
 
   (** Basic borrows  *)
   Axiom lft_borrow_create :
-    ∀ `(nclose lftN ⊆ E) κ P, ▷ P ={E}=★ &{κ} P ★ κ ∋ ▷ P.
+    ∀ `(nclose lftN ⊆ E) κ P, ▷ P ={E}=∗ &{κ} P ∗ κ ∋ ▷ P.
   Axiom lft_borrow_split :
-    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ★ Q) ={E}=★ &{κ}P ★ &{κ}Q.
+    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}(P ∗ Q) ={E}=∗ &{κ}P ∗ &{κ}Q.
   Axiom lft_borrow_combine :
-    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ★ &{κ}Q ={E}=★ &{κ}(P ★ Q).
+    ∀ `(nclose lftN ⊆ E) κ P Q, &{κ}P ∗ &{κ}Q ={E}=∗ &{κ}(P ∗ Q).
   Axiom lft_borrow_acc_strong :
     ∀ `(nclose lftN ⊆ E) q κ P,
-      &{κ}P ⊢ q.[κ] ={E}=★ ▷ P ★
-      ∀ Q, ▷ Q ★ ▷([†κ] ★ ▷Q  ={⊤ ∖ nclose lftN}=★ ▷ P) ={E}=★ &{κ}Q ★ q.[κ].
+      &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗
+      ∀ Q, ▷ Q ∗ ▷([†κ] ∗ ▷Q  ={⊤ ∖ nclose lftN}=∗ ▷ P) ={E}=∗ &{κ}Q ∗ q.[κ].
   Axiom lft_reborrow_static :
     ∀ `(nclose lftN ⊆ E) κ κ' P, κ ≼ κ' →
-      &{κ}P ={E}=★ &{κ'}P ★ κ' ∋ &{κ}P.
+      &{κ}P ={E}=∗ &{κ'}P ∗ κ' ∋ &{κ}P.
   (* FIXME : the document says that we need κ tokens here. Why so?
      Why not κ' tokens also?*)
   Axiom lft_borrow_unnest :
@@ -172,16 +172,16 @@ Section lft.
 
   (** Extraction  *)
   Axiom lft_extract_split :
-    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ (P ★ Q) ={E}=★ κ ∋ P ★ κ ∋ Q.
+    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ (P ∗ Q) ={E}=∗ κ ∋ P ∗ κ ∋ Q.
   Axiom lft_extract_combine :
-    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ P ★ κ ∋ Q ={E}=★ κ ∋ (P ★ Q).
-  Axiom lft_extract_out : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ⊢ κ ∋ P ={E}=★ P.
-  Axiom lft_extract_contravar : ∀ κ P Q, (P -★ Q) ★ κ ∋ P ⊢ κ ∋ Q.
+    ∀ `(nclose lftN ⊆ E) κ P Q, κ ∋ P ∗ κ ∋ Q ={E}=∗ κ ∋ (P ∗ Q).
+  Axiom lft_extract_out : ∀ `(nclose lftN ⊆ E) κ P, [†κ] ⊢ κ ∋ P ={E}=∗ P.
+  Axiom lft_extract_contravar : ∀ κ P Q, (P -∗ Q) ∗ κ ∋ P ⊢ κ ∋ Q.
   Axiom lft_extract_mono : ∀ κ κ' P, κ' ≼ κ → κ ∋ P ⊢ κ' ∋ P.
 
   (*** Derived lemmas  *)
 
-  Lemma lft_own_dead q κ : q.[κ] ★ [† κ] ⊢ False.
+  Lemma lft_own_dead q κ : q.[κ] ∗ [† κ] ⊢ False.
   Proof.
     rewrite /lft_own /lft_dead.
     iIntros "[Hl Hr]". iDestruct "Hr" as (Λ) "[HΛ Hr]".
@@ -191,13 +191,13 @@ Section lft.
     by rewrite lookup_op lookup_singleton lookup_fmap lookup_omap HΛ.
   Qed.
 
-  Lemma lft_own_static q : True ==★ q.[static].
+  Lemma lft_own_static q : True ==∗ q.[static].
   Proof.
     rewrite /lft_own /static omap_empty fmap_empty.
     apply (own_empty (A:=lft_tokUR) toks_name).
   Qed.
 
-  Lemma lft_own_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ★ (q/2).[κ].
+  Lemma lft_own_split κ q : q.[κ] ⊣⊢ (q/2).[κ] ∗ (q/2).[κ].
   Proof. by rewrite -lft_own_frac_op Qp_div_2. Qed.
 
   Global Instance into_and_lft_own_half κ q :
@@ -229,7 +229,7 @@ Section lft.
   Proof. by rewrite /FromSep lft_own_op. Qed.
 
   Lemma lft_borrow_acc E q κ P : nclose lftN ⊆ E →
-      &{κ}P ⊢ q.[κ] ={E}=★ ▷ P ★ (▷ P ={E}=★ &{κ}P ★ q.[κ]).
+      &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ (▷ P ={E}=∗ &{κ}P ∗ q.[κ]).
   Proof.
     iIntros (?) "HP Htok".
     iMod (lft_borrow_acc_strong with "HP Htok") as "[HP Hclose]". done.
@@ -238,7 +238,7 @@ Section lft.
 
   Lemma lft_borrow_exists {A} `(nclose lftN ⊆ E)
         κ q (Φ : A → iProp Σ) {_:Inhabited A}:
-    &{κ}(∃ x, Φ x) ⊢ q.[κ] ={E}=★ ∃ x, &{κ}Φ x ★ q.[κ].
+    &{κ}(∃ x, Φ x) ⊢ q.[κ] ={E}=∗ ∃ x, &{κ}Φ x ∗ q.[κ].
   Proof.
     iIntros "Hb Htok".
     iMod (lft_borrow_acc_strong with "Hb Htok") as "[HΦ Hob]". done.
@@ -246,14 +246,14 @@ Section lft.
   Qed.
 
   Lemma lft_borrow_or `(nclose lftN ⊆ E) κ q P Q:
-    &{κ}(P ∨ Q) ⊢ q.[κ] ={E}=★ (&{κ}P ∨ &{κ}Q) ★ q.[κ].
+    &{κ}(P ∨ Q) ⊢ q.[κ] ={E}=∗ (&{κ}P ∨ &{κ}Q) ∗ q.[κ].
   Proof.
     iIntros "H Htok". rewrite uPred.or_alt.
     iMod (lft_borrow_exists with "H Htok") as ([]) "[H $]"; auto.
   Qed.
 
   Lemma lft_borrow_persistent `(nclose lftN ⊆ E) `{PersistentP _ P} κ q:
-    &{κ}P ⊢ q.[κ] ={E}=★ ▷ P ★ q.[κ].
+    &{κ}P ⊢ q.[κ] ={E}=∗ ▷ P ∗ q.[κ].
   Proof.
     iIntros "Hb Htok".
     iMod (lft_borrow_acc with "Hb Htok") as "[#HP Hob]". done.
@@ -267,7 +267,7 @@ Typeclasses Opaque lft_borrow.
 (*** Inclusion and shortening. *)
 
 Definition lft_incl `{lifetimeG Σ} κ κ' : iProp Σ :=
-  (□ ∀ q, q.[κ] ={lftN}=★ ∃ q', q'.[κ'] ★ (q'.[κ'] ={lftN}=★ q.[κ]))%I.
+  (□ ∀ q, q.[κ] ={lftN}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={lftN}=∗ q.[κ]))%I.
 
 Infix "⊑" := lft_incl (at level 60, right associativity) : C_scope.
 
@@ -277,7 +277,7 @@ Section incl.
   Global Instance lft_incl_persistent κ κ': PersistentP (κ ⊑ κ') := _.
 
   Lemma lft_incl_acc `(nclose lftN ⊆ E) κ κ' q:
-    κ ⊑ κ' ⊢ q.[κ] ={E}=★ ∃ q', q'.[κ'] ★ (q'.[κ'] ={E}=★ q.[κ]).
+    κ ⊑ κ' ⊢ q.[κ] ={E}=∗ ∃ q', q'.[κ'] ∗ (q'.[κ'] ={E}=∗ q.[κ]).
   Proof.
     iIntros "#H Hq". iApply fupd_mask_mono. eassumption.
     iMod ("H" with "*Hq") as (q') "[Hq' Hclose]". iExists q'.
@@ -293,7 +293,7 @@ Section incl.
   Lemma lft_incl_relf κ : True ⊢ κ ⊑ κ.
   Proof. by apply lft_le_incl. Qed.
 
-  Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ★ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
+  Lemma lft_incl_trans κ κ' κ'': κ ⊑ κ' ∗ κ' ⊑ κ'' ⊢ κ ⊑ κ''.
   Proof.
     unfold lft_incl. iIntros "[#H1 #H2]!#*Hκ".
     iMod ("H1" with "*Hκ") as (q') "[Hκ' Hclose]".
@@ -303,15 +303,15 @@ Section incl.
   Qed.
 
   Axiom lft_idx_borrow_shorten :
-    ∀ κ κ' i P, κ ⊑ κ' ⊢ lft_idx_borrow κ' i P -★ lft_idx_borrow κ i P.
+    ∀ κ κ' i P, κ ⊑ κ' ⊢ lft_idx_borrow κ' i P -∗ lft_idx_borrow κ i P.
 
-  Lemma lft_borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -★ &{κ}P.
+  Lemma lft_borrow_shorten κ κ' P: κ ⊑ κ' ⊢ &{κ'}P -∗ &{κ}P.
   Proof.
     iIntros "H⊑ H". unfold lft_borrow. iDestruct "H" as (i) "[??]".
     iExists i. iFrame. by iApply (lft_idx_borrow_shorten with "H⊑").
   Qed.
 
-  Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ★ κ ⊑ κ'' ⊢ κ ⊑ κ' ⋅ κ''.
+  Lemma lft_incl_lb κ κ' κ'' : κ ⊑ κ' ∗ κ ⊑ κ'' ⊢ κ ⊑ κ' ⋅ κ''.
   Proof.
     iIntros "[#H⊑1 #H⊑2]!#". iIntros (q). iIntros "[Hκ'1 Hκ'2]".
     iMod ("H⊑1" with "*Hκ'1") as (q') "[Hκ' Hclose']".
@@ -331,12 +331,12 @@ Section incl.
   Qed.
 
   Lemma lft_reborrow `(nclose lftN ⊆ E) P κ κ':
-    κ' ⊑ κ ⊢ &{κ}P ={E}=★ &{κ'}P ★ κ' ∋ &{κ}P.
+    κ' ⊑ κ ⊢ &{κ}P ={E}=∗ &{κ'}P ∗ κ' ∋ &{κ}P.
   Proof.
     iIntros "#H⊑ HP". iMod (lft_reborrow_static with "HP") as "[Hκ' H∋]".
       done. by exists κ'.
     iDestruct (lft_borrow_shorten with "[H⊑] Hκ'") as "$".
-    { iApply lft_incl_lb. iSplit. done. iApply lft_incl_relf. }
+    { iApply lft_incl_lb. iSplit. done. iIntros "!#*". iApply lft_incl_relf. }
     iApply lft_extract_mono; last by iFrame; auto. exists κ. by rewrite comm.
   Qed.
 
@@ -348,7 +348,7 @@ Typeclasses Opaque lft_incl.
 
 (** Shared borrows  *)
 Definition lft_shr_borrow `{lifetimeG Σ} κ (P : iProp Σ) :=
-  (∃ i, lft_idx_borrow κ i P ★ lft_idx_borrow_persist i)%I.
+  (∃ i, lft_idx_borrow κ i P ∗ lft_idx_borrow_persist i)%I.
 Notation "&shr{ κ } P" := (lft_shr_borrow κ P)
   (format "&shr{ κ } P", at level 20, right associativity) : uPred_scope.
 
@@ -360,21 +360,21 @@ Section shared_borrows.
   Proof. solve_proper. Qed.
   Global Instance lft_shr_borrow_persistent : PersistentP (&shr{κ} P) := _.
 
-  Lemma lft_borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=★ &shr{κ}P.
+  Lemma lft_borrow_share `(nclose lftN ⊆ E) κ : &{κ}P ={E}=∗ &shr{κ}P.
   Proof.
     iIntros "HP". unfold lft_borrow. iDestruct "HP" as (i) "(#?&Hown)".
     iExists i. iMod (lft_idx_borrow_persist_upd with "[$Hown]"). done. by auto.
   Qed.
 
   Lemma lft_shr_borrow_acc `(nclose lftN ⊆ E) q κ :
-    &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=★ ▷P ★ (▷P ={E∖lftN,E}=★ q.[κ]).
+    &shr{κ}P ⊢ q.[κ] ={E,E∖lftN}=∗ ▷P ∗ (▷P ={E∖lftN,E}=∗ q.[κ]).
   Proof.
     iIntros "#HP Hκ". iDestruct "HP" as (i) "(#Hidx&#Hpers)".
     iMod (lft_idx_borrow_persist_acc with "Hidx Hpers Hκ") as "[$H]". done.
     iApply "H".
   Qed.
 
-  Lemma lft_shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -★ &shr{κ}P.
+  Lemma lft_shr_borrow_shorten κ κ': κ ⊑ κ' ⊢ &shr{κ'}P -∗ &shr{κ}P.
   Proof.
     iIntros "#H⊑ H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
       by iApply (lft_idx_borrow_shorten with "H⊑").
@@ -386,8 +386,8 @@ Typeclasses Opaque lft_shr_borrow.
 
 (** Fractured borrows  *)
 Definition lft_frac_borrow `{lifetimeG Σ} κ (Φ : Qp → iProp Σ) :=
-  (∃ γ κ', κ ⊑ κ' ★ &shr{κ'} ∃ q, Φ q ★ own γ q ★
-                       (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ★ q'.[κ']))%I.
+  (∃ γ κ', κ ⊑ κ' ∗ &shr{κ'} ∃ q, Φ q ∗ own γ q ∗
+                       (q = 1%Qp ∨ ∃ q', (q + q')%Qp = 1%Qp ∗ q'.[κ']))%I.
 Notation "&frac{ κ } P" := (lft_frac_borrow κ P)
   (format "&frac{ κ } P", at level 20, right associativity) : uPred_scope.
 
@@ -396,7 +396,7 @@ Section frac_borrow.
   Context `{lifetimeG Σ}.
 
   Lemma lft_borrow_fracture `(nclose lftN ⊆ E) q κ φ:
-    &{κ}(φ 1%Qp) ★ q.[κ] ={E}=★ &frac{κ}φ ★ q.[κ].
+    &{κ}(φ 1%Qp) ∗ q.[κ] ={E}=∗ &frac{κ}φ ∗ q.[κ].
   Proof.
     iIntros "[Hφ Hκ]". iMod (own_alloc 1%Qp) as (γ) "?". done.
     iMod (lft_borrow_acc_strong with "Hφ Hκ") as "[Hφ Hclose]". done.
@@ -410,8 +410,8 @@ Section frac_borrow.
   Qed.
 
   Lemma lft_frac_borrow_acc `(nclose lftN ⊆ E) q κ φ:
-    □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ★ φ q2) ⊢
-    &frac{κ}φ -★ q.[κ] ={E}=★ ∃ q', ▷ φ q' ★ (▷ φ q' ={E}=★ q.[κ]).
+    □ (∀ q1 q2, φ (q1+q2)%Qp ↔ φ q1 ∗ φ q2) ⊢
+    &frac{κ}φ -∗ q.[κ] ={E}=∗ ∃ q', ▷ φ q' ∗ (▷ φ q' ={E}=∗ q.[κ]).
   Proof.
     iIntros "#Hφ Hfrac Hκ". unfold lft_frac_borrow.
     iDestruct "Hfrac" as (γ κ') "#[#Hκκ' Hshr]".
@@ -420,7 +420,7 @@ Section frac_borrow.
     iDestruct "H" as (qφ) "(Hφqφ & >Hown & Hq)".
     destruct (Qp_lower_bound (qκ'/2) (qφ/2)) as (qq & qκ'0 & qφ0 & Hqκ' & Hqφ).
     iExists qq.
-    iAssert (▷ φ qq ★ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
+    iAssert (▷ φ qq ∗ ▷ φ (qφ0 + qφ / 2))%Qp%I with "[Hφqφ]" as "[$ Hqφ]".
     { iNext. rewrite -{1}(Qp_div_2 qφ) {1}Hqφ. iApply "Hφ". by rewrite assoc. }
     rewrite -{1}(Qp_div_2 qφ) {1}Hqφ -assoc {1}Hqκ'.
     iDestruct "Hκ2" as "[Hκq Hκqκ0]". iDestruct "Hown" as "[Hownq Hown]".
@@ -455,7 +455,7 @@ Section frac_borrow.
       iApply "Hclose". rewrite -{2}(Qp_div_2 qκ') {2}Hqκ' !lft_own_frac_op. by iFrame.
   Qed.
 
-  Lemma lft_frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -★ &frac{κ}φ.
+  Lemma lft_frac_borrow_shorten κ κ' φ: κ ⊑ κ' ⊢ &frac{κ'}φ -∗ &frac{κ}φ.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (γ κ0) "[H⊑?]". iExists γ, κ0. iFrame.
     iApply lft_incl_trans. iFrame.
@@ -469,7 +469,7 @@ Typeclasses Opaque lft_frac_borrow.
 
 Definition lft_tl_borrow `{lifetimeG Σ, thread_localG Σ}
            (κ : lifetime) (tid : thread_id) (N : namespace) (P : iProp Σ) :=
-  (∃ i, lft_idx_borrow κ i P ★ tl_inv tid N (lft_idx_borrow_own i))%I.
+  (∃ i, lft_idx_borrow κ i P ∗ tl_inv tid N (lft_idx_borrow_own i))%I.
 
 Notation "&tl{ κ | tid | N } P" := (lft_tl_borrow κ tid N P)
   (format "&tl{ κ | tid | N } P", at level 20, right associativity) : uPred_scope.
@@ -485,7 +485,7 @@ Section tl_borrows.
     intros P1 P2 EQ. apply uPred.exist_proper. intros i. by rewrite EQ.
   Qed.
 
-  Lemma lft_borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=★ &tl{κ|tid|N}P.
+  Lemma lft_borrow_tl κ `(nclose lftN ⊆ E): &{κ}P ={E}=∗ &tl{κ|tid|N}P.
   Proof.
     iIntros "HP". unfold lft_borrow. iDestruct "HP" as (i) "[#? Hown]".
     iExists i. iFrame "#". iApply (tl_inv_alloc tid E N with "[Hown]"). auto.
@@ -493,8 +493,8 @@ Section tl_borrows.
 
   Lemma lft_tl_borrow_acc q κ E F :
     nclose lftN ⊆ E → nclose tlN ⊆ E → nclose N ⊆ F →
-    &tl{κ|tid|N}P ⊢ q.[κ] ★ tl_own tid F ={E}=★ ▷P ★ tl_own tid (F ∖ N) ★
-                     (▷P ★ tl_own tid (F ∖ N) ={E}=★ q.[κ] ★ tl_own tid F).
+    &tl{κ|tid|N}P ⊢ q.[κ] ∗ tl_own tid F ={E}=∗ ▷P ∗ tl_own tid (F ∖ N) ∗
+                     (▷P ∗ tl_own tid (F ∖ N) ={E}=∗ q.[κ] ∗ tl_own tid F).
   Proof.
     iIntros (???) "#HP[Hκ Htlown]".
     iDestruct "HP" as (i) "(#Hpers&#Hinv)".
@@ -504,7 +504,7 @@ Section tl_borrows.
     iMod ("Hclose'" with "HP") as "[Hown $]". iApply "Hclose". by iFrame.
   Qed.
 
-  Lemma lft_tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -★ &tl{κ|tid|N}P.
+  Lemma lft_tl_borrow_shorten κ κ': κ ⊑ κ' ⊢ &tl{κ'|tid|N}P -∗ &tl{κ|tid|N}P.
   Proof.
     iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
     iApply (lft_idx_borrow_shorten with "Hκκ' H").
diff --git a/theories/lifting.v b/theories/lifting.v
index a6646a45..26ba40bd 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -25,12 +25,12 @@ Proof. exact: weakestpre.wp_bind. Qed.
 Lemma wp_alloc_pst E σ n:
   0 < n →
   {{{ ▷ ownP σ }}} Alloc (Lit $ LitInt n) @ E
-  {{{ l σ'; LitV $ LitLoc l,
-      ■ (∀ m, σ !! (shift_loc l m) = None) ★
-      ■ (∃ vl, n = length vl ∧ init_mem l vl σ = σ') ★
+  {{{ l σ', RET LitV $ LitLoc l;
+      ■ (∀ m, σ !! (shift_loc l m) = None) ∗
+      ■ (∃ vl, n = length vl ∧ init_mem l vl σ = σ') ∗
       ownP σ' }}}.
 Proof.
-  iIntros (? Φ) "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
+  iIntros (? Φ) "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ"; iFrame; eauto.
 Qed.
@@ -39,36 +39,36 @@ Lemma wp_free_pst E σ l n :
   0 < n →
   (∀ m, is_Some (σ !! (shift_loc l m)) ↔ (0 ≤ m < n)) →
   {{{ ▷ ownP σ }}} Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E
-  {{{ ; LitV $ LitUnit, ownP (free_mem l (Z.to_nat n) σ) }}}.
+  {{{ RET LitV $ LitUnit; ownP (free_mem l (Z.to_nat n) σ) }}}.
 Proof.
-  iIntros (???)  "[HP HΦ]". iApply (wp_lift_atomic_head_step _ σ); eauto.
+  iIntros (???)  "HP HΦ". iApply (wp_lift_atomic_head_step _ σ); eauto.
   iFrame "HP". iNext. iIntros (v2 σ2 ef) "[% HP]". inv_head_step.
   rewrite big_sepL_nil right_id. by iApply "HΦ".
 Qed.
 
 Lemma wp_read_sc_pst E σ l n v :
   σ !! l = Some (RSt n, v) →
-  {{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ ; v, ownP σ }}}.
+  {{{ ▷ ownP σ }}} Read ScOrd (Lit $ LitLoc l) @ E {{{ RET v; ownP σ }}}.
 Proof.
-  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto using to_of_val.
-  rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
+  rewrite big_sepL_nil right_id; iFrame.
 Qed.
 
 Lemma wp_read_na2_pst E σ l n v :
   σ !! l = Some(RSt $ S n, v) →
   {{{ ▷ ownP σ }}} Read Na2Ord (Lit $ LitLoc l) @ E
-  {{{ ; v, ownP (<[l:=(RSt n, v)]>σ) }}}.
+  {{{ RET v; ownP (<[l:=(RSt n, v)]>σ) }}}.
 Proof.
-  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto using to_of_val.
-  rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
+  rewrite big_sepL_nil right_id; iFrame.
 Qed.
 
 Lemma wp_read_na1_pst E l Φ :
   (|={E,∅}=> ∃ σ n v, σ !! l = Some(RSt $ n, v) ∧
-     ▷ ownP σ ★
-     ▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=★
+     ▷ ownP σ ∗
+     ▷ (ownP (<[l:=(RSt $ S n, v)]>σ) ={∅,E}=∗
           WP Read Na2Ord (Lit $ LitLoc l) @ E {{ Φ }}))
   ⊢ WP Read Na1Ord (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
@@ -81,27 +81,25 @@ Qed.
 Lemma wp_write_sc_pst E σ l v v' :
   σ !! l = Some (RSt 0, v') →
   {{{ ▷ ownP σ }}} Write ScOrd (Lit $ LitLoc l) (of_val v) @ E
-  {{{ ; LitV LitUnit, ownP (<[l:=(RSt 0, v)]>σ) }}}.
+  {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
 Proof.
-  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
+  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
   by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
-  iNext. iIntros "?!>". by iApply "HΦ".
 Qed.
 
 Lemma wp_write_na2_pst E σ l v v' :
   σ !! l = Some(WSt, v') →
   {{{ ▷ ownP σ }}} Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E
-  {{{ ; LitV LitUnit, ownP (<[l:=(RSt 0, v)]>σ) }}}.
+  {{{ RET LitV LitUnit; ownP (<[l:=(RSt 0, v)]>σ) }}}.
 Proof.
-  iIntros (??) "[?HΦ]". iApply wp_lift_atomic_det_head_step; eauto.
-  by intros; inv_head_step; eauto.
-  rewrite big_sepL_nil right_id; iFrame. iNext. iIntros "?!>". by iApply "HΦ".
+  iIntros (??) "?HΦ". iApply wp_lift_atomic_det_head_step; eauto.
+  by intros; inv_head_step; eauto. rewrite big_sepL_nil right_id; iFrame.
 Qed.
 
 Lemma wp_write_na1_pst E l v Φ :
   (|={E,∅}=> ∃ σ v', σ !! l = Some(RSt 0, v') ∧
-     ▷ ownP σ ★
-     ▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=★
+     ▷ ownP σ ∗
+     ▷ (ownP (<[l:=(WSt, v')]>σ) ={∅,E}=∗
        WP Write Na2Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}))
   ⊢ WP Write Na1Ord (Lit $ LitLoc l) (of_val v) @ E {{ Φ }}.
 Proof.
@@ -116,11 +114,11 @@ Lemma wp_cas_fail_pst E σ l n e1 v1 v2 vl :
   σ !! l = Some (RSt n, vl) →
   value_eq σ v1 vl = Some false →
   {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
-  {{{ ; LitV $ LitInt 0, ownP σ }}}.
+  {{{ RET LitV $ LitInt 0; ownP σ }}}.
 Proof.
-  iIntros (?%of_to_val ???) "[HP HΦ]". subst.
+  iIntros (?%of_to_val ???) "HP HΦ". subst.
   iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
-  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?!>". by iApply "HΦ".
+  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?". by iApply "HΦ".
 Qed.
 
 Lemma wp_cas_suc_pst E σ l e1 v1 v2 vl :
@@ -128,18 +126,18 @@ Lemma wp_cas_suc_pst E σ l e1 v1 v2 vl :
   σ !! l = Some (RSt 0, vl) →
   value_eq σ v1 vl = Some true →
   {{{ ▷ ownP σ }}} CAS (Lit $ LitLoc l) e1 (of_val v2) @ E
-  {{{ ; LitV $ LitInt 1, ownP (<[l:=(RSt 0, v2)]>σ) }}}.
+  {{{ RET LitV $ LitInt 1; ownP (<[l:=(RSt 0, v2)]>σ) }}}.
 Proof.
-  iIntros (?%of_to_val ???) "[HP HΦ]". subst.
+  iIntros (?%of_to_val ???) "HP HΦ". subst.
   iApply wp_lift_atomic_det_head_step; eauto. by intros; inv_head_step; eauto.
-  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?!>". by iApply "HΦ".
+  iFrame. iNext. rewrite big_sepL_nil right_id. iIntros "?". by iApply "HΦ".
 Qed.
 
 (** Base axioms for core primitives of the language: Stateless reductions *)
 Lemma wp_fork E e :
-  {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ ; LitV LitUnit, True }}}.
+  {{{ â–· WP e {{ _, True }} }}} Fork e @ E {{{ RET LitV LitUnit; True }}}.
 Proof.
-  iIntros (?) "[?HΦ]". iApply wp_lift_pure_det_head_step; eauto.
+  iIntros (?) "?HΦ". iApply wp_lift_pure_det_head_step; eauto.
   by intros; inv_head_step; eauto. iNext.
   rewrite big_sepL_singleton. iFrame. iApply wp_value. done. by iApply "HΦ".
 Qed.
diff --git a/theories/memcpy.v b/theories/memcpy.v
index e67c0922..18e414be 100644
--- a/theories/memcpy.v
+++ b/theories/memcpy.v
@@ -20,9 +20,9 @@ Notation "e1 <-[ i ]{ n } ! e2" :=
 Lemma wp_memcpy `{heapG Σ} E l1 l2 vl1 vl2 q n:
   nclose heapN ⊆ E →
   length vl1 = n → length vl2 = n →
-  {{{ heap_ctx ★ l1 ↦★ vl1 ★ l2 ↦★{q} vl2 }}}
+  {{{ heap_ctx ∗ l1 ↦∗ vl1 ∗ l2 ↦∗{q} vl2 }}}
     #l1 <-{n} !#l2 @ E
-  {{{; #(), l1 ↦★ vl2 ★ l2 ↦★{q} vl2 }}}.
+  {{{; #(), l1 ↦∗ vl2 ∗ l2 ↦∗{q} vl2 }}}.
 Proof.
   iIntros (? Hvl1 Hvl2 Φ) "[(#Hinv & Hl1 & Hl2) HΦ]".
   iLöb as "IH" forall (n l1 l2 vl1 vl2 Hvl1 Hvl2). wp_rec. wp_op=> ?; wp_if.
diff --git a/theories/perm.v b/theories/perm.v
index 6aeab7ae..0c75b87b 100644
--- a/theories/perm.v
+++ b/theories/perm.v
@@ -27,7 +27,7 @@ Section perm.
     λ tid, (κ ∋ ρ tid)%I.
 
   Definition tok (κ : lifetime) (q : Qp) : perm :=
-    λ _, ([κ]{q} ★ lft κ)%I.
+    λ _, ([κ]{q} ∗ lft κ)%I.
 
   Definition incl (κ κ' : lifetime) : perm :=
     λ _, (κ ⊑ κ')%I.
@@ -36,7 +36,7 @@ Section perm.
     λ tid, (∃ x, P x tid)%I.
 
   Definition sep (ρ1 ρ2 : perm) : @perm Σ :=
-    λ tid, (ρ1 tid ★ ρ2 tid)%I.
+    λ tid, (ρ1 tid ∗ ρ2 tid)%I.
 
   Global Instance top : Top (@perm Σ) :=
     λ _, True%I.
@@ -60,7 +60,7 @@ Infix "⊑" := incl (at level 70) : perm_scope.
 Notation "∃ x .. y , P" :=
   (exist (λ x, .. (exist (λ y, P)) ..)) : perm_scope.
 
-Infix "★" := sep (at level 80, right associativity) : perm_scope.
+Infix "∗" := sep (at level 80, right associativity) : perm_scope.
 
 Section duplicable.
 
@@ -77,7 +77,7 @@ Section duplicable.
   Proof. intros tid. apply _. Qed.
 
   Global Instance sep_dup P Q :
-    Duplicable P → Duplicable Q → Duplicable (P ★ Q).
+    Duplicable P → Duplicable Q → Duplicable (P ∗ Q).
   Proof. intros HP HQ tid. apply _. Qed.
 
   Global Instance top_dup : Duplicable ⊤.
@@ -98,7 +98,7 @@ Section has_type.
   Qed.
 
   Lemma has_type_wp E (ν : expr) ty tid (Φ : val -> iProp _) :
-    (ν ◁ ty)%P tid ★ (∀ (v : val), eval_expr ν = Some v ★ (v ◁ ty)%P tid ={E}=★ Φ v)
+    (ν ◁ ty)%P tid ∗ (∀ (v : val), eval_expr ν = Some v ∗ (v ◁ ty)%P tid ={E}=∗ Φ v)
     ⊢ WP ν @ E {{ Φ }}.
   Proof.
     iIntros "[H◁ HΦ]". setoid_rewrite has_type_value. unfold has_type.
diff --git a/theories/perm_incl.v b/theories/perm_incl.v
index 20f49864..5fd49048 100644
--- a/theories/perm_incl.v
+++ b/theories/perm_incl.v
@@ -10,13 +10,13 @@ Section defs.
 
   (* Definitions *)
   Definition perm_incl (ρ1 ρ2 : perm) :=
-    ∀ tid, ρ1 tid ={⊤}=★ ρ2 tid.
+    ∀ tid, ρ1 tid ={⊤}=∗ ρ2 tid.
 
   Global Instance perm_equiv : Equiv perm :=
     λ ρ1 ρ2, perm_incl ρ1 ρ2 ∧ perm_incl ρ2 ρ1.
 
   Definition borrowing κ (ρ ρ1 ρ2 : perm) :=
-    ∀ tid, lft κ ⊢ ρ tid -★ ρ1 tid ={⊤}=★ ρ2 tid ★ κ ∋ ρ1 tid.
+    ∀ tid, lft κ ⊢ ρ tid -∗ ρ1 tid ={⊤}=∗ ρ2 tid ∗ κ ∋ ρ1 tid.
 
 End defs.
 
@@ -65,11 +65,11 @@ Section props.
   Lemma perm_incl_top ρ : ρ ⇒ ⊤.
   Proof. iIntros (tid) "H". eauto. Qed.
 
-  Lemma perm_incl_frame_l ρ ρ1 ρ2 : ρ1 ⇒ ρ2 → ρ ★ ρ1 ⇒ ρ ★ ρ2.
+  Lemma perm_incl_frame_l ρ ρ1 ρ2 : ρ1 ⇒ ρ2 → ρ ∗ ρ1 ⇒ ρ ∗ ρ2.
   Proof. iIntros (Hρ tid) "[$?]". by iApply Hρ. Qed.
 
   Lemma perm_incl_frame_r ρ ρ1 ρ2 :
-    ρ1 ⇒ ρ2 → ρ1 ★ ρ ⇒ ρ2 ★ ρ.
+    ρ1 ⇒ ρ2 → ρ1 ∗ ρ ⇒ ρ2 ∗ ρ.
   Proof. iIntros (Hρ tid) "[?$]". by iApply Hρ. Qed.
 
   Lemma perm_incl_exists_intro {A} P x : P x ⇒ ∃ x : A, P x.
@@ -87,11 +87,11 @@ Section props.
   Global Instance perm_top_left_id : LeftId (⇔) ⊤ sep.
   Proof. intros ρ. by rewrite comm right_id. Qed.
 
-  Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ★ ρ.
+  Lemma perm_incl_duplicable ρ (_ : Duplicable ρ) : ρ ⇒ ρ ∗ ρ.
   Proof. iIntros (tid) "#H!>". by iSplit. Qed.
 
   Lemma perm_tok_plus κ q1 q2 :
-    tok κ q1 ★ tok κ q2 ⇔ tok κ (q1 + q2).
+    tok κ q1 ∗ tok κ q2 ⇔ tok κ (q1 + q2).
   Proof.
     rewrite /tok /sep /=; split; intros tid; rewrite -lft_own_op;
       iIntros "[[$$]H]!>". by iDestruct "H" as "[$?]". by auto.
@@ -100,11 +100,11 @@ Section props.
   Lemma perm_lftincl_refl κ : ⊤ ⇒ κ ⊑ κ.
   Proof. iIntros (tid) "_!>". iApply lft_incl_refl. Qed.
 
-  Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ★ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
+  Lemma perm_lftincl_trans κ1 κ2 κ3 : κ1 ⊑ κ2 ∗ κ2 ⊑ κ3 ⇒ κ1 ⊑ κ3.
   Proof. iIntros (tid) "[#?#?]!>". iApply lft_incl_trans. auto. Qed.
 
   Lemma perm_incl_share q ν κ ty :
-    ν ◁ &uniq{κ} ty ★ [κ]{q} ⇒ ν ◁ &shr{κ} ty ★ [κ]{q}.
+    ν ◁ &uniq{κ} ty ∗ [κ]{q} ⇒ ν ◁ &shr{κ} ty ∗ [κ]{q}.
   Proof.
     iIntros (tid) "[Huniq [Htok $]]". unfold has_type.
     destruct (eval_expr ν); last by iDestruct "Huniq" as "[]".
@@ -117,14 +117,14 @@ Section props.
   Lemma split_own_prod tyl (q0: Qp) (ql : list Qp) (l : loc) tid :
     length tyl = length ql →
       (own (foldr Qp_plus q0 ql) (Π tyl)).(ty_own) tid [ #l] ⊣⊢
-    ▷ †{q0}(shift_loc l (0 + (Π tyl).(ty_size))%nat)…0 ★
-    [★ list] qtyoffs ∈ (combine ql (combine_offs tyl 0)),
+    ▷ †{q0}(shift_loc l (0 + (Π tyl).(ty_size))%nat)…0 ∗
+    [∗ list] qtyoffs ∈ (combine ql (combine_offs tyl 0)),
          (own (qtyoffs.1) (qtyoffs.2.1)).(ty_own)
               tid [ #(shift_loc l (qtyoffs.2.2))].
   Proof.
     intros Hlen.
     assert (REW: ∀ (l : loc) (Φ : loc → iProp Σ),
-               Φ l ⊣⊢ (∃ l0:loc, [ #l] = [ #l0] ★ Φ l0)).
+               Φ l ⊣⊢ (∃ l0:loc, [ #l] = [ #l0] ∗ Φ l0)).
     { intros l0 Φ. iSplit; iIntros "H". eauto.
       iDestruct "H" as (l') "[Heq H]". iDestruct "Heq" as %[=]. subst. done. }
     setoid_rewrite <-REW. clear REW.
@@ -145,7 +145,7 @@ Section props.
     foldr (λ (q : Qp) acc, q + acc)%Qc 0%Qc ql = q →
     ν ◁ own q (Π tyl) ⇔
       foldr (λ qtyoffs acc,
-             (ν +ₗ #(qtyoffs.2.2:nat))%E ◁ own (qtyoffs.1) (qtyoffs.2.1) ★ acc)
+             (ν +ₗ #(qtyoffs.2.2:nat))%E ◁ own (qtyoffs.1) (qtyoffs.2.1) ∗ acc)
             ⊤ (combine ql (combine_offs tyl 0)).
   Proof.
     intros Hlen Hq. assert (ql ≠ []).
@@ -168,7 +168,7 @@ Section props.
       apply uPred.exist_proper=>l0.
       rewrite -{3}(Qp_div_2 q0) -{3}(right_id O plus ty.(ty_size))
               -heap_freeable_op_eq uPred.later_sep -!assoc.
-      iSplit; iIntros "[#Eq[?[??]]]"; iFrame "# ★";
+      iSplit; iIntros "[#Eq[?[??]]]"; iFrame "# ∗";
         iDestruct "Eq" as %[=]; subst; rewrite shift_loc_assoc_nat //.
     - rewrite /= big_sepL_cons /sep -IH // !uPred.sep_exist_r uPred.sep_exist_l.
       apply uPred.exist_proper=>l0. rewrite -!assoc /=.
@@ -178,7 +178,7 @@ Section props.
   Lemma perm_split_uniq_borrow_prod tyl κ ν :
     ν ◁ &uniq{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
-             (ν +ₗ #(tyoffs.2:nat))%E ◁ &uniq{κ} (tyoffs.1) ★ acc)%P
+             (ν +ₗ #(tyoffs.2:nat))%E ◁ &uniq{κ} (tyoffs.1) ∗ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
     intros tid. unfold has_type. simpl eval_expr.
@@ -195,7 +195,7 @@ Section props.
   Lemma perm_split_shr_borrow_prod tyl κ ν :
     ν ◁ &shr{κ} (Π tyl) ⇒
       foldr (λ tyoffs acc,
-             (ν +ₗ #(tyoffs.2:nat))%E ◁ &shr{κ} (tyoffs.1) ★ acc)%P
+             (ν +ₗ #(tyoffs.2:nat))%E ◁ &shr{κ} (tyoffs.1) ∗ acc)%P
             ⊤ (combine_offs tyl 0).
   Proof.
     intros tid. unfold has_type. simpl eval_expr.
@@ -213,7 +213,7 @@ Section props.
   Admitted.
 
   Lemma borrowing_perm_incl κ ρ ρ1 ρ2 θ :
-    borrowing κ ρ ρ1 ρ2 → ρ ★ κ ∋ θ ★ ρ1 ⇒ ρ2 ★ κ ∋ (θ ★ ρ1).
+    borrowing κ ρ ρ1 ρ2 → ρ ∗ κ ∋ θ ∗ ρ1 ⇒ ρ2 ∗ κ ∋ (θ ∗ ρ1).
   Proof.
     iIntros (Hbor tid) "(Hρ&Hθ&Hρ1)".
     iMod (Hbor with "[#] Hρ Hρ1") as "[$ ?]". by iApply lft_extract_lft.
@@ -251,7 +251,7 @@ Section props.
   Qed.
 
   Lemma reborrow_shr_perm_incl κ κ' ν ty :
-    κ ⊑ κ' ★ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
+    κ ⊑ κ' ∗ ν ◁ &shr{κ'}ty ⇒ ν ◁ &shr{κ}ty.
   Proof.
     iIntros (tid) "[#Hord #Hκ']". unfold has_type.
     destruct (eval_expr ν) as [[[|l|]|]|];
diff --git a/theories/proofmode.v b/theories/proofmode.v
index 1b135df1..ade46392 100644
--- a/theories/proofmode.v
+++ b/theories/proofmode.v
@@ -17,20 +17,20 @@ Global Instance into_and_mapsto l q v :
 Proof. by rewrite /IntoAnd heap_mapsto_op_split. Qed.
 
 Global Instance into_and_mapsto_vec l q vl :
-  IntoAnd false (l ↦★{q} vl) (l ↦★{q/2} vl) (l ↦★{q/2} vl).
+  IntoAnd false (l ↦∗{q} vl) (l ↦∗{q/2} vl) (l ↦∗{q/2} vl).
 Proof. by rewrite /IntoAnd heap_mapsto_vec_op_split. Qed.
 
 Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → 0 < n →
   IntoLaterEnvs Δ Δ' →
   (∀ l vl, n = length vl → ∃ Δ'',
-    envs_app false (Esnoc (Esnoc Enil j1 (l ↦★ vl)) j2 (†l…(Z.to_nat n))) Δ'
+    envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
       = Some Δ'' ∧
     (Δ'' ⊢ |={E}=> Φ (LitV $ LitLoc l))) →
   Δ ⊢ WP Alloc (Lit $ LitInt n) @ E {{ Φ }}.
 Proof.
-  intros ???? HΔ. rewrite -wp_fupd -wp_alloc // -always_and_sep_l.
-  apply and_intro; first done.
+  intros ???? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
+  rewrite -always_and_sep_l. apply and_intro; first done.
   rewrite into_later_env_sound; apply later_mono, forall_intro=> l;
   apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
   apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
@@ -41,7 +41,7 @@ Qed.
 Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   (Δ ⊢ heap_ctx) → nclose heapN ⊆ E → n = length vl →
   IntoLaterEnvs Δ Δ' →
-  envs_lookup i1 Δ' = Some (false, l ↦★ vl)%I →
+  envs_lookup i1 Δ' = Some (false, l ↦∗ vl)%I →
   envs_delete i1 false Δ' = Δ'' →
   envs_lookup i2 Δ'' = Some (false, †l…n')%I →
   envs_delete i2 false Δ'' = Δ''' →
@@ -49,8 +49,8 @@ Lemma tac_wp_free Δ Δ' Δ'' Δ''' E i1 i2 vl (n : Z) (n' : nat) l Φ :
   (Δ''' ⊢ |={E}=> Φ (LitV LitUnit)) →
   Δ ⊢ WP Free (Lit $ LitInt n) (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
-  intros ?? -> ?? <- ? <- -> HΔ.
-  rewrite -wp_fupd -wp_free // -!assoc -always_and_sep_l.
+  intros ?? -> ?? <- ? <- -> HΔ. rewrite -wp_fupd.
+  eapply wand_apply; first exact:wp_free. rewrite -!assoc -always_and_sep_l.
   apply and_intro; first done.
   rewrite into_later_env_sound -!later_sep; apply later_mono.
   do 2 (rewrite envs_lookup_sound' //). by rewrite HΔ wand_True.
@@ -64,12 +64,12 @@ Lemma tac_wp_read Δ Δ' E i l q v o Φ :
   Δ ⊢ WP Read o (Lit $ LitLoc l) @ E {{ Φ }}.
 Proof.
   intros ??[->| ->]???.
-  - rewrite -wp_fupd -wp_read_na // -!assoc -always_and_sep_l.
-    apply and_intro; first done.
+  - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_na.
+    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_fupd -wp_read_sc // -!assoc -always_and_sep_l.
-    apply and_intro; first done.
+  - rewrite -wp_fupd. eapply wand_apply; first exact:wp_read_sc.
+    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
       by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -84,10 +84,12 @@ Lemma tac_wp_write Δ Δ' Δ'' E i l v e v' o Φ :
   Δ ⊢ WP Write o (Lit $ LitLoc l) e @ E {{ Φ }}.
 Proof.
   intros ???[->| ->]????.
-  - rewrite -wp_fupd -wp_write_na // -!assoc -always_and_sep_l. apply and_intro; first done.
+  - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_na.
+    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
-  - rewrite -wp_fupd -wp_write_sc // -!assoc -always_and_sep_l. apply and_intro; first done.
+  - rewrite -wp_fupd. eapply wand_apply; first by apply wp_write_sc.
+    rewrite -!assoc -always_and_sep_l. apply and_intro; first done.
     rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
     rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -135,8 +137,8 @@ Tactic Notation "wp_free" :=
       |solve_ndisj
       |try fast_done
       |apply _
-      |let l := match goal with |- _ = Some (_, (?l ↦★ _)%I) => l end in
-       iAssumptionCore || fail "wp_free: cannot find" l "↦★ ?"
+      |let l := match goal with |- _ = Some (_, (?l ↦∗ _)%I) => l end in
+       iAssumptionCore || fail "wp_free: cannot find" l "↦∗ ?"
       |env_cbv; reflexivity
       |let l := match goal with |- _ = Some (_, († ?l … _)%I) => l end in
        iAssumptionCore || fail "wp_free: cannot find †" l "… ?"
diff --git a/theories/type.v b/theories/type.v
index 3ef012f9..029c5090 100644
--- a/theories/type.v
+++ b/theories/type.v
@@ -33,14 +33,14 @@ Record type `{heapG Σ, lifetimeG Σ, thread_localG Σ} :=
        more consistent with thread-local tokens, which we do not
        give any. *)
     ty_share E N κ l tid q : mgmtE ⊥ nclose N → mgmtE ⊆ E →
-      &{κ} (l ↦★: ty_own tid) ⊢ [κ]{q} ={E}=★ ty_shr κ tid N l ★ [κ]{q};
+      &{κ} (l ↦∗: ty_own tid) ⊢ [κ]{q} ={E}=∗ ty_shr κ tid N l ∗ [κ]{q};
     ty_shr_mono κ κ' tid N l :
       κ' ⊑ κ ⊢ ty_shr κ tid N l → ty_shr κ' tid N l;
     ty_shr_acc κ tid E N l q :
       ty_dup → mgmtE ∪ nclose N ⊆ E →
       ty_shr κ tid N l ⊢
-        [κ]{q} ★ tl_own tid N ={E}=★ ∃ q', ▷l ↦★{q'}: ty_own tid ★
-           (▷l ↦★{q'}: ty_own tid ={E}=★ [κ]{q} ★ tl_own tid N)
+        [κ]{q} ∗ tl_own tid N ={E}=∗ ∃ q', ▷l ↦∗{q'}: ty_own tid ∗
+           (▷l ↦∗{q'}: ty_own tid ={E}=∗ [κ]{q} ∗ tl_own tid N)
   }.
 Global Existing Instances ty_shr_persistent ty_dup_persistent.
 
@@ -61,7 +61,7 @@ Program Coercion ty_of_st `{heapG Σ, lifetimeG Σ, thread_localG Σ}
         borrow, otherwise I do not knwo how to prove the shr part of
         [lft_incl_ty_incl_shared_borrow]. *)
      ty_shr := λ κ tid _ l,
-               (∃ vl, (&frac{κ} λ q, l ↦★{q} vl) ★ ▷ st.(st_own) tid vl)%I
+               (∃ vl, (&frac{κ} λ q, l ↦∗{q} vl) ∗ ▷ st.(st_own) tid vl)%I
   |}.
 Next Obligation. intros. apply st_size_eq. Qed.
 Next Obligation.
@@ -142,11 +142,11 @@ Section types.
 
             Since this assertion is timeless, this should not cause
             problems. *)
-         (∃ l:loc, vl = [ #l ] ★ ▷ †{q}l…ty.(ty_size)
-                               ★ ▷ l ↦★: ty.(ty_own) tid)%I;
+         (∃ l:loc, vl = [ #l ] ∗ ▷ †{q}l…ty.(ty_size)
+                               ∗ ▷ l ↦∗: ty.(ty_own) tid)%I;
        ty_shr κ tid N l :=
-         (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ★
-            ∀ q', □ ([κ]{q'} ={mgmtE ∪ N, mgmtE}▷=★ ty.(ty_shr) κ tid N l' ★ [κ]{q'}))%I
+         (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
+            ∀ q', □ ([κ]{q'} ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ tid N l' ∗ [κ]{q'}))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -169,7 +169,7 @@ Section types.
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iAssert (&{κ}▷ l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
+    - iAssert (&{κ}▷ l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
       { iApply lft_borrow_persist. eauto. }
       iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
       iIntros "!>". iNext.
@@ -194,11 +194,11 @@ Section types.
   Program Definition uniq_borrow (κ:lifetime) (ty:type) :=
     {| ty_size := 1; ty_dup := false;
        ty_own tid vl :=
-         (∃ l:loc, vl = [ #l ] ★ &{κ} l ↦★: ty.(ty_own) tid)%I;
+         (∃ l:loc, vl = [ #l ] ∗ &{κ} l ↦∗: ty.(ty_own) tid)%I;
        ty_shr κ' tid N l :=
-         (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ★
-            ∀ q' κ'', □ (κ'' ⊑ κ ★ κ'' ⊑ κ' ★ [κ'']{q'}
-               ={mgmtE ∪ N, mgmtE}▷=★ ty.(ty_shr) κ'' tid N l' ★ [κ'']{q'}))%I
+         (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
+            ∀ q' κ'', □ (κ'' ⊑ κ ∗ κ'' ⊑ κ' ∗ [κ'']{q'}
+               ={mgmtE ∪ N, mgmtE}▷=∗ ty.(ty_shr) κ'' tid N l' ∗ [κ'']{q'}))%I
     |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -222,8 +222,8 @@ Section types.
     iMod (inv_open with "Hinv") as "[INV Hclose]". set_solver.
     replace ((mgmtE ∪ N) ∖ N) with mgmtE by set_solver.
     iDestruct "INV" as "[>Hbtok|#Hshr]".
-    - iAssert (&{κ''}&{κ} l' ↦★: ty_own ty tid)%I with "[Hbtok]" as "Hb".
-      { iApply lft_borrow_persist. iExists κ0, i. iFrame "★ #".
+    - iAssert (&{κ''}&{κ} l' ↦∗: ty_own ty tid)%I with "[Hbtok]" as "Hb".
+      { iApply lft_borrow_persist. iExists κ0, i. iFrame "∗ #".
         iApply lft_incl_trans. eauto. }
       iMod (lft_borrow_open with "Hb Htok") as "[Hown Hob]". set_solver.
       iIntros "!>". iNext.
@@ -255,7 +255,7 @@ Section types.
 
   Program Definition shared_borrow (κ : lifetime) (ty : type) : type :=
     {| st_size := 1;
-       st_own tid vl := (∃ l:loc, vl = [ #l ] ★ ty.(ty_shr) κ tid lrustN l)%I |}.
+       st_own tid vl := (∃ l:loc, vl = [ #l ] ∗ ty.(ty_shr) κ tid lrustN l)%I |}.
   Next Obligation.
     iIntros (κ ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.
   Qed.
@@ -268,7 +268,7 @@ Section types.
 
   Lemma list_ty_type_eq tid (tyl : list type) (vll : list (list val)) :
     length tyl = length vll →
-    ([★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))
+    ([∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))
       ⊢ length (concat vll) = sum_list_with ty_size tyl.
   Proof.
     revert vll; induction tyl as [|ty tyq IH]; destruct vll;
@@ -279,11 +279,11 @@ Section types.
   Qed.
 
   Lemma split_prod_mt tid tyl l q :
-    (l ↦★{q}: λ vl,
-       ∃ vll, vl = concat vll ★ length tyl = length vll
-         ★ [★ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I
-    ⊣⊢ [★ list] tyoffs ∈ combine_offs tyl 0,
-         shift_loc l (tyoffs.2) ↦★{q}: ty_own (tyoffs.1) tid.
+    (l ↦∗{q}: λ vl,
+       ∃ vll, vl = concat vll ∗ length tyl = length vll
+         ∗ [∗ list] tyvl ∈ combine tyl vll, ty_own (tyvl.1) tid (tyvl.2))%I
+    ⊣⊢ [∗ list] tyoffs ∈ combine_offs tyl 0,
+         shift_loc l (tyoffs.2) ↦∗{q}: ty_own (tyoffs.1) tid.
   Proof.
     rewrite -{1}(shift_loc_0_nat l). generalize 0%nat.
     induction tyl as [|ty tyl IH]=>/= offs.
@@ -317,7 +317,7 @@ Section types.
 
   Lemma split_prod_namespace tid (N : namespace) n :
     ∃ E, (tl_own tid N ⊣⊢ tl_own tid E
-                 ★ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ★ P) 0%nat n)
+                 ∗ nat_rec_shift True (λ i P, tl_own tid (N .@ i) ∗ P) 0%nat n)
          ∧ (∀ i, i < 0 → nclose (N .@ i) ⊆ E)%nat.
   Proof.
     generalize 0%nat. induction n as [|n IH].
@@ -333,15 +333,15 @@ Section types.
   Program Definition product (tyl : list type) :=
     {| ty_size := sum_list_with ty_size tyl; ty_dup := forallb ty_dup tyl;
        ty_own tid vl :=
-         (∃ vll, vl = concat vll ★ length tyl = length vll ★
-                 [★ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
+         (∃ vll, vl = concat vll ∗ length tyl = length vll ∗
+                 [∗ list] tyvl ∈ combine tyl vll, tyvl.1.(ty_own) tid (tyvl.2))%I;
        ty_shr κ tid N l :=
-         ([★ list] i ↦ tyoffs ∈ combine_offs tyl 0,
+         ([∗ list] i ↦ tyoffs ∈ combine_offs tyl 0,
            tyoffs.1.(ty_shr) κ tid (N .@ i) (shift_loc l (tyoffs.2)))%I
     |}.
   Next Obligation.
     intros tyl tid vl Hfa.
-    cut (∀ vll, PersistentP ([★ list] tyvl ∈ combine tyl vll,
+    cut (∀ vll, PersistentP ([∗ list] tyvl ∈ combine tyl vll,
                              ty_own (tyvl.1) tid (tyvl.2))). by apply _.
     clear vl. induction tyl as [|ty tyl IH]=>[|[|vl vll]]; try by apply _.
     edestruct andb_prop_elim as [Hduph Hdupq]. by apply Hfa.
@@ -387,7 +387,7 @@ Section types.
       iExists q'. iModIntro. rewrite big_sepL_cons.
       rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
       iDestruct "Hownh" as "[$ Hownh1]".
-      rewrite (big_sepL_proper (λ _ x, _ ↦★{_}: _)%I); last first.
+      rewrite (big_sepL_proper (λ _ x, _ ↦∗{_}: _)%I); last first.
       { intros. rewrite -heap_mapsto_vec_prop_op; last apply ty_size_eq.
         instantiate (1:=λ _ y, _). simpl. reflexivity. }
       rewrite big_sepL_sepL. iDestruct "Hownq" as "[$ Hownq1]".
@@ -397,9 +397,9 @@ Section types.
   Qed.
 
   Lemma split_sum_mt l tid q tyl :
-    (l ↦★{q}: λ vl,
-         ∃ (i : nat) vl', vl = #i :: vl' ★ ty_own (nth i tyl emp) tid vl')%I
-    ⊣⊢ ∃ (i : nat), l ↦{q} #i ★ shift_loc l 1 ↦★{q}: ty_own (nth i tyl emp) tid.
+    (l ↦∗{q}: λ vl,
+         ∃ (i : nat) vl', vl = #i :: vl' ∗ ty_own (nth i tyl emp) tid vl')%I
+    ⊣⊢ ∃ (i : nat), l ↦{q} #i ∗ shift_loc l 1 ↦∗{q}: ty_own (nth i tyl emp) tid.
   Proof.
     iSplit; iIntros "H".
     - iDestruct "H" as (vl) "[Hmt Hown]". iDestruct "Hown" as (i vl') "(%&Hown)". subst.
@@ -428,9 +428,9 @@ Section types.
   Program Definition sum {n} (tyl : list type) {_:LstTySize n tyl} :=
     {| ty_size := S n; ty_dup := forallb ty_dup tyl;
        ty_own tid vl :=
-         (∃ (i : nat) vl', vl = #i :: vl' ★ (nth i tyl emp).(ty_own) tid vl')%I;
+         (∃ (i : nat) vl', vl = #i :: vl' ∗ (nth i tyl emp).(ty_own) tid vl')%I;
        ty_shr κ tid N l :=
-         (∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ★
+         (∃ (i : nat), (&frac{κ} λ q, l ↦{q} #i) ∗
                (nth i tyl emp).(ty_shr) κ tid N (shift_loc l 1))%I
     |}.
   Next Obligation.
@@ -489,9 +489,9 @@ Section types.
 
   Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
     {| ty_size := 1; ty_dup := false;
-       ty_own tid vl := (∃ f, vl = [f] ★
-          ∀ vl, ρ vl tid -★ tl_own tid ⊤
-                 -★ WP f (map of_val vl) {{λ _, False}})%I;
+       ty_own tid vl := (∃ f, vl = [f] ∗
+          ∀ vl, ρ vl tid -∗ tl_own tid ⊤
+                 -∗ WP f (map of_val vl) {{λ _, False}})%I;
        ty_shr κ tid N l := True%I |}.
   Next Obligation. done. Qed.
   Next Obligation.
@@ -507,8 +507,8 @@ Section types.
      needs a Send closure). *)
   Program Definition fn {A n} (ρ : A -> vec val n → @perm Σ) : type :=
     {| st_size := 1;
-       st_own tid vl := (∃ f, vl = [f] ★ ∀ x vl,
-         {{ ρ x vl tid ★ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
+       st_own tid vl := (∃ f, vl = [f] ∗ ∀ x vl,
+         {{ ρ x vl tid ∗ tl_own tid ⊤ }} f (map of_val vl) {{λ _, False}})%I |}.
   Next Obligation.
     iIntros (x n ρ tid vl) "H". iDestruct "H" as (f) "[% _]". by subst.
   Qed.
diff --git a/theories/type_incl.v b/theories/type_incl.v
index ce370a7f..82619adb 100644
--- a/theories/type_incl.v
+++ b/theories/type_incl.v
@@ -9,20 +9,20 @@ Section ty_incl.
   Context `{heapG Σ, lifetimeG Σ, thread_localG Σ}.
 
   Definition ty_incl (ρ : perm) (ty1 ty2 : type) :=
-    ∀ tid, ρ tid ={⊤}=★
-      (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ★
+    ∀ tid, ρ tid ={⊤}=∗
+      (□ ∀ vl, ty1.(ty_own) tid vl → ty2.(ty_own) tid vl) ∗
       (□ ∀ κ E l, ty1.(ty_shr) κ tid E l →
        (* [ty_incl] needs to prove something about the length of the
           object when it is shared. We place this property under the
           hypothesis that [ty2.(ty_shr)] holds, so that the [!] type
           is still included in any other. *)
-                  ty2.(ty_shr) κ tid E l ★ ty1.(ty_size) = ty2.(ty_size)).
+                  ty2.(ty_shr) κ tid E l ∗ ty1.(ty_size) = ty2.(ty_size)).
 
   Global Instance ty_incl_refl ρ : Reflexive (ty_incl ρ).
   Proof. iIntros (ty tid) "_!>". iSplit; iIntros "!#"; eauto. Qed.
 
   Lemma ty_incl_trans ρ θ ty1 ty2 ty3 :
-    ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ★ θ) ty1 ty3.
+    ty_incl ρ ty1 ty2 → ty_incl θ ty2 ty3 → ty_incl (ρ ∗ θ) ty1 ty3.
   Proof.
     iIntros (H12 H23 tid) "[H1 H2]".
     iMod (H12 with "H1") as "[#H12 #H12']".
@@ -93,10 +93,10 @@ Section ty_incl.
     Duplicable ρ → Forall2 (ty_incl ρ) tyl1 tyl2 → ty_incl ρ (Π tyl1) (Π tyl2).
   Proof.
     intros Hρ HFA. iIntros (tid) "#Hρ". iSplitL "".
-    - assert (Himpl : ρ tid ={⊤}=★
+    - assert (Himpl : ρ tid ={⊤}=∗
          □ (∀ vll, length tyl1 = length vll →
-               ([★ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
-             → ([★ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
+               ([∗ list] tyvl ∈ combine tyl1 vll, ty_own (tyvl.1) tid (tyvl.2))
+             → ([∗ list] tyvl ∈ combine tyl2 vll, ty_own (tyvl.1) tid (tyvl.2)))).
       { induction HFA as [|ty1 ty2 tyl1 tyl2 Hincl HFA IH].
         - iIntros "_!>!#* _ _". by rewrite big_sepL_nil.
         - iIntros "#Hρ". iMod (IH with "Hρ") as "#Hqimpl".
@@ -147,7 +147,7 @@ Section ty_incl.
     ty_incl ρ (sum tyl1) (sum tyl2).
   Proof.
     iIntros (DUP FA tid) "#Hρ". rewrite /sum /=. iSplitR "".
-    - assert (Hincl : ρ tid ={⊤}=★
+    - assert (Hincl : ρ tid ={⊤}=∗
          (□ ∀ i vl, (nth i tyl1 ∅%T).(ty_own) tid vl
                   → (nth i tyl2 ∅%T).(ty_own) tid vl)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
@@ -157,7 +157,7 @@ Section ty_incl.
       iMod (Hincl with "Hρ") as "#Hincl". iIntros "!>!#*H".
       iDestruct "H" as (i vl') "[% Hown]". subst. iExists _, _. iSplit. done.
         by iApply "Hincl".
-    - assert (Hincl : ρ tid ={⊤}=★
+    - assert (Hincl : ρ tid ={⊤}=∗
          (□ ∀ i κ E l, (nth i tyl1 ∅%T).(ty_shr) κ tid E l
                      → (nth i tyl2 ∅%T).(ty_shr) κ tid E l)).
       { clear -FA DUP. induction FA as [|ty1 ty2 tyl1 tyl2 Hincl _ IH].
@@ -197,7 +197,7 @@ Section ty_incl.
   Admitted.
 
   Lemma ty_incl_cont {n} ρ ρ1 ρ2 :
-    Duplicable ρ → (∀ vl : vec val n, ρ ★ ρ2 vl ⇒ ρ1 vl) →
+    Duplicable ρ → (∀ vl : vec val n, ρ ∗ ρ2 vl ⇒ ρ1 vl) →
     ty_incl ρ (cont ρ1) (cont ρ2).
   Proof.
     iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*H"; last by auto.
@@ -207,7 +207,7 @@ Section ty_incl.
   Qed.
 
   Lemma ty_incl_fn {A n} ρ ρ1 ρ2 :
-    Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ★ ρ2 x vl ⇒ ρ1 x vl) →
+    Duplicable ρ → (∀ (x : A) (vl : vec val n), ρ ∗ ρ2 x vl ⇒ ρ1 x vl) →
     ty_incl ρ (fn ρ1) (fn ρ2).
   Proof.
     iIntros (? Hρ1ρ2 tid) "#Hρ!>". iSplit; iIntros "!#*#H".
@@ -242,7 +242,7 @@ Section ty_incl.
   Qed.
 
   Lemma ty_incl_perm_incl ρ ty1 ty2 ν :
-    ty_incl ρ ty1 ty2 → ρ ★ ν ◁ ty1 ⇒ ν ◁ ty2.
+    ty_incl ρ ty1 ty2 → ρ ∗ ν ◁ ty1 ⇒ ν ◁ ty2.
   Proof.
     iIntros (Hincl tid) "[Hρ Hty1]". iMod (Hincl with "Hρ") as "[#Hownincl _]".
     unfold Perm.has_type. destruct (Perm.eval_expr ν); last done. by iApply "Hownincl".
diff --git a/theories/typing.v b/theories/typing.v
index 8e407a82..a5db5e09 100644
--- a/theories/typing.v
+++ b/theories/typing.v
@@ -10,24 +10,24 @@ Section typing.
 
   (* TODO : good notations for [typed_step] and [typed_step_ty] ? *)
   Definition typed_step (ρ : perm) e (θ : val → perm) :=
-    ∀ tid, {{ heap_ctx ★ ρ tid ★ tl_own tid ⊤ }} e
-           {{ v, θ v tid ★ tl_own tid ⊤ }}.
+    ∀ tid, {{ heap_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e
+           {{ v, θ v tid ∗ tl_own tid ⊤ }}.
 
   Definition typed_step_ty (ρ : perm) e ty :=
     typed_step ρ e (λ ν, ν ◁ ty)%P.
 
   Definition typed_program (ρ : perm) e :=
-    ∀ tid, {{ heap_ctx ★ ρ tid ★ tl_own tid ⊤ }} e {{ _, False }}.
+    ∀ tid, {{ heap_ctx ∗ ρ tid ∗ tl_own tid ⊤ }} e {{ _, False }}.
 
   Lemma typed_frame ρ e θ ξ:
-    typed_step ρ e θ → typed_step (ρ ★ ξ) e (λ ν, θ ν ★ ξ)%P.
+    typed_step ρ e θ → typed_step (ρ ∗ ξ) e (λ ν, θ ν ∗ ξ)%P.
   Proof.
     iIntros (Hwt tid) "!#(#HEAP&[?$]&?)". iApply Hwt. by iFrame.
   Qed.
 
   Lemma typed_step_exists {A} ρ θ e ξ:
-    (∀ x:A, typed_step (ρ ★ θ x) e ξ) →
-    typed_step (ρ ★ ∃ x, θ x) e ξ.
+    (∀ x:A, typed_step (ρ ∗ θ x) e ξ) →
+    typed_step (ρ ∗ ∃ x, θ x) e ξ.
   Proof.
     iIntros (Hwt tid) "!#(#HEAP&[Hρ Hθ]&?)". iDestruct "Hθ" as (x) "Hθ".
     iApply Hwt. by iFrame.
@@ -44,7 +44,7 @@ Section typing.
     length xl = n →
     (∀ (a : A) (vl : vec val n) (fv : val) e',
         subst_l xl (map of_val vl) e = Some e' →
-        typed_program (fv ◁ fn θ ★ (θ a vl) ★ ρ) (subst' f fv e')) →
+        typed_program (fv ◁ fn θ ∗ (θ a vl) ∗ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (fn θ).
   Proof.
     iIntros (Hn He tid) "!#(#HEAP&#Hρ&$)".
@@ -57,14 +57,14 @@ Section typing.
     iApply wp_rec; try done.
     { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
       rewrite to_of_val. eauto. }
-    iNext. iApply He. done. iFrame "★#". by rewrite has_type_value.
+    iNext. iApply He. done. iFrame "∗#". by rewrite has_type_value.
   Qed.
 
   Lemma typed_cont {n} `{Closed (f :b: xl +b+ []) e} ρ θ :
     length xl = n →
     (∀ (fv : val) (vl : vec val n) e',
         subst_l xl (map of_val vl) e = Some e' →
-        typed_program (fv ◁ cont (λ vl, ρ ★ θ vl)%P ★ (θ vl) ★ ρ) (subst' f fv e')) →
+        typed_program (fv ◁ cont (λ vl, ρ ∗ θ vl)%P ∗ (θ vl) ∗ ρ) (subst' f fv e')) →
     typed_step_ty ρ (Rec f xl e) (cont θ).
   Proof.
     iIntros (Hn He tid) "!#(#HEAP&Hρ&$)". specialize (He (RecV f xl e)).
@@ -77,7 +77,7 @@ Section typing.
     iApply wp_rec; try done.
     { apply List.Forall_forall=>?. rewrite in_map_iff=>-[?[<- _]].
       rewrite to_of_val. eauto. }
-    iNext. iApply He. done. iFrame "★#". rewrite has_type_value.
+    iNext. iApply He. done. iFrame "∗#". rewrite has_type_value.
     iExists _. iSplit. done. iIntros (vl') "[Hρ Hθ] Htl".
     iDestruct ("IH" with "Hρ") as (f') "[Hf' IH']".
     iDestruct "Hf'" as %[=<-]. iApply ("IH'" with "Hθ Htl").
@@ -91,7 +91,7 @@ Section typing.
 
   Lemma typed_plus e1 e2 ρ1 ρ2:
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ★ ρ2) (e1 + e2) int.
+    typed_step_ty (ρ1 ∗ ρ2) (e1 + e2) int.
   Proof.
     unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
     iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
@@ -104,7 +104,7 @@ Section typing.
 
   Lemma typed_minus e1 e2 ρ1 ρ2:
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ★ ρ2) (e1 - e2) int.
+    typed_step_ty (ρ1 ∗ ρ2) (e1 - e2) int.
   Proof.
     unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
     iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
@@ -117,7 +117,7 @@ Section typing.
 
   Lemma typed_le e1 e2 ρ1 ρ2:
     typed_step_ty ρ1 e1 int → typed_step_ty ρ2 e2 int →
-    typed_step_ty (ρ1 ★ ρ2) (e1 ≤ e2) bool.
+    typed_step_ty (ρ1 ∗ ρ2) (e1 ≤ e2) bool.
   Proof.
     unfold typed_step_ty, typed_step. setoid_rewrite has_type_value.
     iIntros (He1 He2 tid) "!#(#HEAP&[H1 H2]&?)".
@@ -129,7 +129,7 @@ Section typing.
   Qed.
 
   Lemma typed_newlft ρ:
-    typed_step ρ Newlft (λ _, ∃ α, [α]{1} ★ α ∋ top)%P.
+    typed_step ρ Newlft (λ _, ∃ α, [α]{1} ∗ α ∋ top)%P.
   Proof.
     iIntros (tid) "!#(_&_&$)". wp_value. iMod lft_begin as (α) "[?#?]". done.
     iMod (lft_borrow_create with "[][]") as "[_?]". done. done.
@@ -137,10 +137,10 @@ Section typing.
   Qed.
 
   Lemma typed_endlft κ ρ:
-    typed_step (κ ∋ ρ ★ [κ]{1}) Endlft (λ _, ρ)%P.
+    typed_step (κ ∋ ρ ∗ [κ]{1}) Endlft (λ _, ρ)%P.
   Proof.
     iIntros (tid) "!#(_&[Hextr [Htok #Hlft]]&$)". wp_bind (#() ;; #())%E.
-    iApply (wp_wand_r _ _ (λ _, _ ★ True)%I). iSplitR "Hextr".
+    iApply (wp_wand_r _ _ (λ _, _ ∗ True)%I). iSplitR "Hextr".
     iApply (wp_frame_step_l with "[-]"); try done.
     iDestruct (lft_end with "Hlft Htok") as "$". by wp_seq.
     iIntros (v) "[#Hκ _]". iMod (lft_extract_out with "Hκ Hextr"). done.
@@ -161,18 +161,18 @@ Section typing.
     iIntros (tid) "!#(#HEAP&H◁&$)". wp_bind ν.
     iApply (has_type_wp with "[$H◁]"). iIntros (v) "[_ H◁]!>".
     rewrite has_type_value.
-    iDestruct "H◁" as (l) "(Hv & >H† & H↦★:)". iDestruct "Hv" as %[=->].
-    iDestruct "H↦★:" as (vl) "[>H↦ Hown]".
+    iDestruct "H◁" as (l) "(Hv & >H† & H↦∗:)". iDestruct "Hv" as %[=->].
+    iDestruct "H↦∗:" as (vl) "[>H↦ Hown]".
     rewrite ty_size_eq. iDestruct "Hown" as ">%". wp_free; eauto.
   Qed.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
-      ρ1 ν tid ★ tl_own tid ⊤ ★
+      ρ1 ν tid ∗ tl_own tid ⊤ ∗
       (∀ (l:loc) vl q,
-        (length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★{q} vl ★
-         |={E}▷=> (ty.(ty_own) tid vl ★ (l ↦★{q} vl ={E}=★ ρ2 ν tid ★ tl_own tid ⊤)))
-       -★ Φ #l)
+        (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗{q} vl ∗
+         |={E}▷=> (ty.(ty_own) tid vl ∗ (l ↦∗{q} vl ={E}=∗ ρ2 ν tid ∗ tl_own tid ⊤)))
+       -∗ Φ #l)
       ⊢ WP ν @ E {{ Φ }}.
 
   Lemma consumes_copy_own ty q:
@@ -184,7 +184,7 @@ Section typing.
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
+    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
     rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
@@ -197,14 +197,14 @@ Section typing.
     iDestruct "Heq" as %[=->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦!>".
+    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦!>".
     rewrite /has_type Hνv. iExists _. iSplit. done. iFrame. iExists vl. eauto.
   Qed.
 
   Lemma consumes_copy_uniq_borrow ty κ κ' q:
     ty.(ty_dup) →
-    consumes ty (λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
-                (λ ν, ν ◁ &uniq{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
+    consumes ty (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
+                (λ ν, ν ◁ &uniq{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
   Proof.
     iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & Htok & #Hκ') & Htl & HΦ)".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
@@ -214,7 +214,7 @@ Section typing.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
+    iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
     iMod (lft_borrow_close with "[H↦] Hclose'") as "[H↦ Htok]". set_solver.
     { iExists _. by iFrame. }
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
@@ -222,8 +222,8 @@ Section typing.
 
   Lemma consumes_copy_shr_borrow ty κ κ' q:
     ty.(ty_dup) →
-    consumes ty (λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P
-                (λ ν, ν ◁ &shr{κ}ty ★ κ' ⊑ κ ★ [κ']{q})%P.
+    consumes ty (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
+                (λ ν, ν ◁ &shr{κ}ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
   Proof.
     iIntros (? ν tid Φ E ?) "((H◁ & #H⊑ & [Htok #Hκ']) & Htl & HΦ)".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
@@ -236,14 +236,14 @@ Section typing.
     iDestruct "H↦" as (vl) "[>H↦ #Hown]".
     iAssert (â–· (length vl = ty_size ty))%I with "[#]" as ">%".
       by rewrite ty.(ty_size_eq).
-    iModIntro. iApply "HΦ". iFrame "★#%". iIntros "!>!>!>H↦".
+    iModIntro. iApply "HΦ". iFrame "∗#%". iIntros "!>!>!>H↦".
     iMod ("Hclose'" with "[H↦]") as "[Htok $]". iExists _; by iFrame.
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
   Qed.
 
   Lemma typed_deref ty ρ1 ρ2 (ν:expr) :
     ty.(ty_size) = 1%nat → consumes ty ρ1 ρ2 →
-    typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ★ ρ2 ν)%P.
+    typed_step (ρ1 ν) (!ν) (λ v, v ◁ ty ∗ ρ2 ν)%P.
   Proof.
     iIntros (Hsz Hconsumes tid) "!#[#HEAP[??]]". wp_bind ν.
     iApply Hconsumes. done. iFrame. iIntros (l vl q) "(%&%&H↦&Hupd)".
@@ -253,9 +253,9 @@ Section typing.
   Qed.
 
   Lemma typed_deref_uniq_borrow_own ty ν κ κ' q q':
-    typed_step (ν ◁ &uniq{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
+    typed_step (ν ◁ &uniq{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
                (!ν)
-               (λ v, v ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
+               (λ v, v ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
   Proof.
     iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
@@ -275,9 +275,9 @@ Section typing.
   Qed.
 
   Lemma typed_deref_shr_borrow_own ty ν κ κ' q q':
-    typed_step (ν ◁ &shr{κ} own q' ty ★ κ' ⊑ κ ★ [κ']{q})
+    typed_step (ν ◁ &shr{κ} own q' ty ∗ κ' ⊑ κ ∗ [κ']{q})
                (!ν)
-               (λ v, v ◁ &shr{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
+               (λ v, v ◁ &shr{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
   Proof.
     iIntros (tid) "!#(#HEAP & (H◁ & #H⊑ & Htok & #Hκ') & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
@@ -288,7 +288,7 @@ Section typing.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
     iSpecialize ("Hown" $! _ with "Htok2").
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
-    - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ★ v = #vl)%I); try done.
+    - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q'''} v ∗ v = #vl)%I); try done.
       iSplitL "Hown"; last by wp_read; eauto.
       iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
         last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
@@ -299,9 +299,9 @@ Section typing.
   Qed.
 
   Lemma typed_deref_uniq_borrow_borrow ty ν κ κ' κ'' q:
-    typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
+    typed_step (ν ◁ &uniq{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
                (!ν)
-               (λ v, v ◁ &uniq{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
+               (λ v, v ◁ &uniq{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
   Proof.
     iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
@@ -322,9 +322,9 @@ Section typing.
   Qed.
 
   Lemma typed_deref_shr_borrow_borrow ty ν κ κ' κ'' q:
-    typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ★ κ ⊑ κ' ★ [κ]{q} ★ κ' ⊑ κ'')
+    typed_step (ν ◁ &shr{κ'} &uniq{κ''} ty ∗ κ ⊑ κ' ∗ [κ]{q} ∗ κ' ⊑ κ'')
                (!ν)
-               (λ v, v ◁ &shr{κ'} ty ★ κ ⊑ κ' ★ [κ]{q})%P.
+               (λ v, v ◁ &shr{κ'} ty ∗ κ ⊑ κ' ∗ [κ]{q})%P.
   Proof.
     iIntros (tid) "!#(#HEAP & (H◁ & #H⊑1 & [Htok #Hκ'] & #H⊑2) & $)". wp_bind ν.
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]!>". iDestruct "Hνv" as %Hνv.
@@ -335,7 +335,7 @@ Section typing.
     { iIntros "!#". iIntros (q1 q2). rewrite heap_mapsto_op_eq. iSplit; auto. }
     iSpecialize ("Hown" $! _ _ with "[$H⊑2 $Htok2]"). iApply lft_incl_refl.
     iApply wp_strong_mono. reflexivity. iSplitL "Hclose Hclose'"; last first.
-    - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ★ v = #l')%I); try done.
+    - iApply (wp_frame_step_l _ heapN _ (λ v, l ↦{q''} v ∗ v = #l')%I); try done.
       iSplitL "Hown"; last by wp_read; eauto.
       iApply step_fupd_mask_mono; last iApply (step_fupd_mask_frame_r _ _ heapN);
         last iApply "Hown"; (set_solver || rewrite !disjoint_union_l; solve_ndisj).
@@ -346,11 +346,11 @@ Section typing.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
     ∀ ν tid Φ E, mgmtE ∪ lrustN ⊆ E →
-      ρ1 ν tid ★
+      ρ1 ν tid ∗
       (∀ (l:loc) vl,
-         (length vl = ty.(ty_size) ★ eval_expr ν = Some #l ★ l ↦★ vl ★
-         ∀ vl', l ↦★ vl' ★ ▷ (ty.(ty_own) tid vl') ={E}=★ ρ2 ν tid)
-         -★ Φ #l)
+         (length vl = ty.(ty_size) ∗ eval_expr ν = Some #l ∗ l ↦∗ vl ∗
+         ∀ vl', l ↦∗ vl' ∗ ▷ (ty.(ty_own) tid vl') ={E}=∗ ρ2 ν tid)
+         -∗ Φ #l)
       ⊢ WP ν @ E {{ Φ }}.
 
   Lemma update_strong ty1 ty2 q:
@@ -361,14 +361,14 @@ Section typing.
     iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
     rewrite has_type_value. iDestruct "H◁" as (l) "(Heq & >H† & H↦)".
     iDestruct "Heq" as %[= ->]. iDestruct "H↦" as (vl) "[>H↦ Hown]".
-    rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "★%".
+    rewrite ty2.(ty_size_eq) -Hsz. iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%".
     iIntros (vl') "[H↦ Hown']!>". rewrite /has_type Hνv.
     iExists _. iSplit. done. iFrame. iExists _. iFrame.
   Qed.
 
   Lemma update_weak ty q κ κ':
-    update ty (λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P
-              (λ ν, ν ◁ &uniq{κ} ty ★ κ' ⊑ κ ★ [κ']{q})%P.
+    update ty (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P
+              (λ ν, ν ◁ &uniq{κ} ty ∗ κ' ⊑ κ ∗ [κ']{q})%P.
   Proof.
     iIntros (ν tid Φ E ?) "[(H◁ & #H⊑ & Htok & #Hκ) HΦ]".
     iApply (has_type_wp with "[- $H◁]"). iIntros (v) "[Hνv H◁]". iDestruct "Hνv" as %Hνv.
@@ -376,7 +376,7 @@ Section typing.
     iMod (lft_incl_trade with "H⊑ Htok") as (q') "[Htok Hclose]". set_solver.
     iMod (lft_borrow_open with "H↦ Htok") as "[H↦ Hclose']". set_solver.
     iDestruct "H↦" as (vl) "[>H↦ Hown]". rewrite ty.(ty_size_eq).
-    iDestruct "Hown" as ">%". iApply "HΦ". iFrame "★%#". iIntros (vl') "[H↦ Hown]".
+    iDestruct "Hown" as ">%". iApply "HΦ". iFrame "∗%#". iIntros (vl') "[H↦ Hown]".
     iMod (lft_borrow_close with "[H↦ Hown] Hclose'") as "[Hbor Htok]". set_solver.
     { iExists _. iFrame. }
     iMod ("Hclose" with "Htok") as "$". rewrite /has_type Hνv. iExists _. eauto.
@@ -384,7 +384,7 @@ Section typing.
 
   Lemma typed_assign ρ1 ρ2 ty ν1 ν2:
     ty.(ty_size) = 1%nat → update ty ρ1 ρ2 →
-    typed_step (ρ1 ν1 ★ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
+    typed_step (ρ1 ν1 ∗ ν2 ◁ ty) (ν1 <- ν2) (λ _, ρ2 ν1).
   Proof.
     iIntros (Hsz Hupd tid) "!#(#HEAP & [Hρ1 H◁] & $)". wp_bind ν1.
     iApply Hupd. done. iFrame. iIntros (l vl) "(%&%&H↦&Hupd)".
@@ -396,14 +396,14 @@ Section typing.
 
   Lemma typed_memcpy ρ1 ρ1' ρ2 ρ2' ty ν1 ν2:
     update ty ρ1' ρ1 → consumes ty ρ2' ρ2 →
-    typed_step (ρ1' ν1 ★ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ★ ρ2 ν2)%P.
+    typed_step (ρ1' ν1 ∗ ρ2' ν2) (ν1 <-{ty.(ty_size)} !ν2) (λ _, ρ1 ν1 ∗ ρ2 ν2)%P.
   Proof.
     iIntros (Hupd Hcons tid) "!#(#HEAP&[H1 H2]&Htl)". wp_bind ν1.
     iApply (Hupd with "[- $H1]"). done.
     iIntros (l vl) "(% & % & H↦ & Hupd)". wp_bind ν2.
     iApply (Hcons with "[- $H2 $Htl]"). done.
     iIntros (l' vl' q) "(% & % & H↦' & Hcons)". iApply wp_fupd.
-    iMod "Hcons". iApply wp_memcpy; last iFrame "★#"; try done. iNext.
+    iMod "Hcons". iApply wp_memcpy; last iFrame "∗#"; try done. iNext.
     iIntros "[H↦ H↦']". iMod "Hcons" as "[Hown' Hcons]".
     iMod ("Hcons" with "H↦'") as "[$$]". iApply "Hupd". by iFrame.
   Qed.
@@ -416,8 +416,8 @@ Section typing.
   Qed.
 
   Lemma typed_program_exists {A} ρ θ e:
-    (∀ x:A, typed_program (ρ ★ θ x) e) →
-    typed_program (ρ ★ ∃ x, θ x) e.
+    (∀ x:A, typed_program (ρ ∗ θ x) e) →
+    typed_program (ρ ∗ ∃ x, θ x) e.
   Proof.
     iIntros (Hwt tid) "!#(#HEAP & [Hρ Hθ] & ?)". iDestruct "Hθ" as (x) "Hθ".
     iApply Hwt. by iFrame.
@@ -435,7 +435,7 @@ Section typing.
 
   Lemma typed_if ρ e1 e2 ν:
     typed_program ρ e1 → typed_program ρ e2 →
-    typed_program (ρ ★ ν ◁ bool) (if: ν then e1 else e2).
+    typed_program (ρ ∗ ν ◁ bool) (if: ν then e1 else e2).
   Proof.
     iIntros (He1 He2 tid) "!#(#HEAP & [Hρ H◁] & Htl)".
     wp_bind ν. iApply has_type_wp. iFrame. iIntros (v) "[% H◁]!>".
-- 
GitLab