diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 8f8b51b22672aa0f225428da6c9be106e6cc5235..7bbe625b5b068dce2eb7b9c3438db298bd5d7de4 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -43,7 +43,7 @@ Section heap.
   Hint Resolve to_heap_valid.
 
   Global Instance heap_inv_proper : Proper ((≡) ==> (≡)) (heap_inv HeapI).
-  Proof. by intros h1 h2; fold_leibniz=> ->. Qed.
+  Proof. intros h1 h2. by fold_leibniz=> ->. Qed.
 
   Lemma heap_own_op γ σ1 σ2 :
     (heap_own HeapI γ σ1 ★ heap_own HeapI γ σ2)%I
@@ -59,7 +59,7 @@ Section heap.
   Proof. (* TODO. *)
   Abort.
 
-  (* TODO: Prove equivalence to a big sum. *)
+  (* TODO: Do we want equivalence to a big sum? *)
 
   Lemma heap_alloc N σ :
     ownP σ ⊑ pvs N N (∃ γ, heap_ctx HeapI γ N ∧ heap_own HeapI γ σ).
@@ -73,7 +73,7 @@ Section heap.
     P ⊑ wp E (Load (Loc l)) Q.
   Proof.
     rewrite /heap_ctx /heap_own. intros HN Hl Hctx HP.
-    eapply (auth_fsa (heap_inv HeapI) (wp_fsa (Load _) _) (λ _, True) id).
+    eapply (auth_fsa (heap_inv HeapI) (wp_fsa (Load _) _) id).
     { eassumption. } { eassumption. }
     rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
     apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 54e802a236657e22f9f7e4b2023a83af1d6912fb..9ab3f954ee6994e63fa5162f2ca46dbe85e37473 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -84,7 +84,7 @@ Section auth.
      step-indices. However, since A is timeless, that should not be
      a restriction.  *)
   Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
-        Lv L `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
+        L `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
     P ⊑ (auth_own AuthI γ a ★ (∀ a', ■✓(a ⋅ a') ★ ▷φ (a ⋅ a') -★