diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index a827cbd4e0e6049b7f1337de690ab00cd37724a1..b427bb5b36f6322cdc4a199b011508b9e2798e62 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -96,7 +96,7 @@ Lemma newbarrier_spec (P : iProp Σ) (Φ : val → iProp Σ) :
   heap_ctx ★ (∀ l, recv l P ★ send l P -★ Φ #l) ⊢ WP newbarrier #() {{ Φ }}.
 Proof.
   iIntros (HN) "[#? HΦ]".
-  rewrite /newbarrier. wp_seq. wp_alloc l as "Hl".
+  rewrite /newbarrier /=. wp_seq. wp_alloc l as "Hl".
   iApply ("HΦ" with "==>[-]").
   iVs (saved_prop_alloc (F:=idCF) P) as (γ) "#?".
   iVs (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
@@ -120,7 +120,7 @@ Qed.
 Lemma signal_spec l P (Φ : val → iProp Σ) :
   send l P ★ P ★ Φ #() ⊢ WP signal #l {{ Φ }}.
 Proof.
-  rewrite /signal /send /barrier_ctx.
+  rewrite /signal /send /barrier_ctx /=.
   iIntros "(Hs&HP&HΦ)"; iDestruct "Hs" as (γ) "[#(%&Hh&Hsts) Hγ]". wp_let.
   iVs (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
     as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 4da10b23024c601819c3da32d4a65c90d23b4ab5..3969f018a8e11472b80575f814867803ec44457b 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -50,7 +50,7 @@ Lemma newlock_spec (R : iProp Σ) Φ :
   heapN ⊥ N →
   heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ #l) ⊢ WP newlock #() {{ Φ }}.
 Proof.
-  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock.
+  iIntros (?) "(#Hh & HR & HΦ)". rewrite /newlock /=.
   wp_seq. wp_alloc l as "Hl".
   iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
@@ -75,7 +75,7 @@ Lemma release_spec R l (Φ : val → iProp Σ) :
   locked l R ★ R ★ Φ #() ⊢ WP release #l {{ Φ }}.
 Proof.
   iIntros "(Hl&HR&HΦ)"; iDestruct "Hl" as (γ) "(% & #? & #? & Hγ)".
-  rewrite /release. wp_let. iInv N as (b) "[Hl _]" "Hclose".
+  rewrite /release /=. wp_let. iInv N as (b) "[Hl _]" "Hclose".
   wp_store. iFrame "HΦ". iApply "Hclose". iNext. iExists false. by iFrame.
 Qed.
 End proof.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index 81195b9d45925781a5ab1d263067d1296b1c09cb..757d89d5e783e80a14366c91374fedb71e3f7ca2 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -52,13 +52,13 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) (Φ : val → iProp Σ) :
   heap_ctx ★ WP f #() {{ Ψ }} ★ (∀ l, join_handle l Ψ -★ Φ #l)
   ⊢ WP spawn e {{ Φ }}.
 Proof.
-  iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn.
+  iIntros (<-%of_to_val ?) "(#Hh & Hf & HΦ)". rewrite /spawn /=.
   (* TODO: Coq is printing %V here.  *)
   wp_let. wp_alloc l as "Hl". wp_let.
   iVs (own_alloc (Excl ())) as (γ) "Hγ"; first done.
   iVs (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
   { iNext. iExists NONEV. iFrame; eauto. }
-  wp_apply wp_fork. iSplitR "Hf".
+  wp_apply wp_fork; simpl. iSplitR "Hf".
   - iVsIntro. wp_seq. iVsIntro. iApply "HΦ". rewrite /join_handle. eauto.
   - wp_bind (f _). iApply wp_wand_l. iFrame "Hf"; iIntros (v) "Hv".
     iInv N as (v') "[Hl _]" "Hclose".
diff --git a/heap_lang/lib/ticket_lock.v b/heap_lang/lib/ticket_lock.v
index 96bef7eafaecad7c9b1540bc488b64de7f54702f..ddc6beebcdf65f5fbdc2146b15bc289ec81476ea 100644
--- a/heap_lang/lib/ticket_lock.v
+++ b/heap_lang/lib/ticket_lock.v
@@ -78,7 +78,7 @@ Proof. apply _. Qed.
 Lemma newlock_spec (R : iProp Σ) Φ :
   heap_ctx ★ R ★ (∀ l, is_lock l R -★ Φ l) ⊢ WP newlock #() {{ Φ }}.
 Proof.
-  iIntros "(#Hh & HR & HΦ)". rewrite /newlock.
+  iIntros "(#Hh & HR & HΦ)". rewrite /newlock /=.
   wp_seq. wp_alloc lo as "Hlo". wp_alloc ln as "Hln".
   iVs (own_alloc (Excl ())) as (γ2) "Hγ2"; first done.
   iVs (own_alloc_strong (Auth (Excl' ∅) ∅) {[ γ2 ]}) as (γ1) "[% Hγ1]"; first done.