diff --git a/heap_lang/lib/lock.v b/heap_lang/lib/lock.v
index 511d3a87e45f5150dc06a8afed7fe15e23ad2443..a74e0ad5f55bf5278e3b6056a811087be2fcff8c 100644
--- a/heap_lang/lib/lock.v
+++ b/heap_lang/lib/lock.v
@@ -52,12 +52,12 @@ Lemma newlock_spec N (R : iProp) Φ :
   (heap_ctx heapN ★ R ★ (∀ l, is_lock l R -★ Φ (LocV l)))
   ⊢ WP newlock #() {{ Φ }}.
 Proof.
-  iIntros {?} "(#Hh&HR&HΦ)". rewrite /newlock.
+  iIntros {?} "(#Hh & HR & HΦ)". rewrite /newlock.
   wp_seq. iApply wp_pvs. wp_alloc l as "Hl".
   iPvs (own_alloc (Excl ())) as {γ} "Hγ"; first done.
-  iPvs (inv_alloc N _ (lock_inv γ l R)) "[HR Hl Hγ]" as "#?"; first done.
+  iPvs (inv_alloc N _ (lock_inv γ l R)) "-[HΦ]" as "#?"; first done.
   { iNext. iExists false. by iFrame "Hl HR". }
-  iPvsIntro; iApply "HΦ". iExists N, γ. by repeat iSplit.
+  iPvsIntro. iApply "HΦ". iExists N, γ. by repeat iSplit.
 Qed.
 
 Lemma acquire_spec l R (Φ : val → iProp) :
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index a897a0827b5b34bbbd76d6a9b49ae6084c430f48..3502c54ba39ca0ef4b7f5a39536b577b84f16f47 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -570,7 +570,7 @@ Qed.
 (** * Rewriting *)
 Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
   envs_lookup i Δ = Some (p, Pxy) →
-  ∀ {A : cofeT} x y (Φ : A → uPred M),
+  ∀ {A : cofeT} (x y : A) (Φ : A → uPred M),
     Pxy ⊢ (x ≡ y)%I →
     Q ⊣⊢ Φ (if lr then y else x) →
     (∀ n, Proper (dist n ==> dist n) Φ) →
@@ -761,7 +761,7 @@ Global Instance or_destruct_later P Q1 Q2 :
 Proof. rewrite /OrDestruct=>->. by rewrite later_or. Qed.
 
 Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
-  envs_lookup i Δ = Some (p, P)%I → OrDestruct P P1 P2 →
+  envs_lookup i Δ = Some (p, P) → OrDestruct P P1 P2 →
   envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
   envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
   Δ1 ⊢ Q → Δ2 ⊢ Q → Δ ⊢ Q.
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index f10a57d99adc64b07130a7af2211f5f1e6edb7b7..853b38f420c454e4a7064477dd835c55a59476a9 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -70,6 +70,6 @@ Section ClosedProofs.
   Proof.
     iProof. iIntros "! Hσ".
     iPvs (heap_alloc nroot) "Hσ" as {h} "[? _]"; first by rewrite nclose_nroot.
-    iApply heap_e_spec; last done ; by rewrite nclose_nroot.
+    iApply heap_e_spec; last done; by rewrite nclose_nroot.
   Qed.
 End ClosedProofs.