diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index fb906f2e513d668c4ce132937aa9735fea4bd3c3..31ab9d3f315bffffde9649c29cb05118129a0f18 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -110,7 +110,7 @@ Proof.
   iAssert (barrier_ctx γ' l P)%I as "#?".
   { rewrite /barrier_ctx. by repeat iSplit. }
   iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ★ sts_ownS γ' low_states {[Send]})%I with "=>[-]" as "[Hr Hs]".
+    ★ sts_ownS γ' low_states {[Send]})%I with "|==>[-]" as "[Hr Hs]".
   { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
     + set_solver.
     + iApply (sts_own_weaken with "Hγ'");
@@ -148,7 +148,7 @@ Proof.
     iExists (State Low I), {[ Change i ]}; iSplit; [done|iSplitL "Hl Hr"].
     { iNext. rewrite {2}/barrier_inv /=. by iFrame. }
     iIntros "Hγ".
-    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "=>[Hγ]" as "Hγ".
+    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "|==>[Hγ]" as "Hγ".
     { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
     wp_op=> ?; simplify_eq; wp_if. iApply ("IH" with "Hγ [HQR] HΦ"). auto.
   - (* a High state: the comparison succeeds, and we perform a transition and
@@ -185,7 +185,7 @@ Proof.
     iApply (ress_split _ _ _ Q R1 R2); eauto. iFrame; auto.
   - iIntros "Hγ".
     iAssert (sts_ownS γ (i_states i1) {[Change i1]}
-      ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "=>[-]" as "[Hγ1 Hγ2]".
+      ★ sts_ownS γ (i_states i2) {[Change i2]})%I with "|==>[-]" as "[Hγ1 Hγ2]".
     { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
       + set_solver.
       + iApply (sts_own_weaken with "Hγ");
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index 8f4e0edfb7c11d95fbbfb57b0c5abc17a5672a89..9f50539601632fac061daa55e05fd2ea1c6449e1 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -193,7 +193,7 @@ Lemma box_empty_all f P Q :
 Proof.
   iIntros {?} "H"; iDestruct "H" as {Φ} "[#HeqP Hf]".
   iAssert ([★ map] γ↦b ∈ f, ▷ Φ γ ★ box_own_auth γ (◯ Excl' false) ★
-    box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "=>[Hf]" as "[HΦ ?]".
+    box_own_prop γ (Φ γ) ★ inv N (slice_inv γ (Φ γ)))%I with "|==>[Hf]" as "[HΦ ?]".
   { iApply (pvs_big_sepM _ _ f); iApply (big_sepM_impl _ _ f); iFrame "Hf".
     iAlways; iIntros {γ b ?} "(Hγ' & #$ & #$)".
     assert (true = b) as <- by eauto.
diff --git a/proofmode/spec_patterns.v b/proofmode/spec_patterns.v
index c6919d5fa41cf24a3a21abba68856ed45021c0cb..4ef97c10b67a210d2ab7c6787ac36b69d22a3d82 100644
--- a/proofmode/spec_patterns.v
+++ b/proofmode/spec_patterns.v
@@ -32,7 +32,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : string) : list token :=
   | String "#" s => tokenize_go s (TPersistent :: cons_name kn k) ""
   | String "%" s => tokenize_go s (TPure :: cons_name kn k) ""
   | String "*" s => tokenize_go s (TForall :: cons_name kn k) ""
-  | String "=" (String ">" s) => tokenize_go s (TPvs :: cons_name kn k) ""
+  | String "|" (String "=" (String "=" (String ">" s))) =>
+     tokenize_go s (TPvs :: cons_name kn k) ""
   | String a s => tokenize_go s k (String a kn)
   end.
 Definition tokenize (s : string) : list token := tokenize_go s [] "".
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 02e9a825ccd5dafcd1b274eeb287ab102798c142..9301a91b987e1e340358babde4dc32b288316388 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -100,7 +100,7 @@ Section iris.
     (True -★ P -★ inv N Q -★ True -★ R) ⊢ P -★ ▷ Q -★ |={E}=> R.
   Proof.
     iIntros {?} "H HP HQ".
-    iApply ("H" with "[#] HP =>[HQ] =>").
+    iApply ("H" with "[#] HP |==>[HQ] |==>").
     - done.
     - by iApply inv_alloc.
     - by iPvsIntro.