diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 1502ce450534da482b5a7d9f58b1feb23c3a2199..d3c948d43076cd86f3a44a9fd111b67919a3dcd5 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -84,7 +84,7 @@ Section LiftingTests.
     True ⊑ wp (Σ:=globalF Σ) E (let: "x" := Pred '42 in Pred "x") (λ v, v = '40).
   Proof.
     intros E.
-    wp_focus (Pred '42); rewrite -Pred_spec -later_intro.
+    wp_focus (Pred _); rewrite -Pred_spec -later_intro.
     wp_rec. rewrite -Pred_spec -later_intro; auto with I.
   Qed.
 End LiftingTests.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index c88954726accc39ab818118b13d7235ed685ab5c..164bb9b487061e111e0b27b2cf8d2186446c50b6 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -4,12 +4,12 @@ Import uPred.
 Ltac wp_strip_later :=
   match goal with
   | |- ∀ _, _ => let H := fresh in intro H; wp_strip_later; revert H
-  | |- _ ⊑ ▷ _ => etransitivity; [|apply later_intro]
+  | |- _ ⊑ ▷ _ => etransitivity; [|by apply later_intro]
   end.
 Ltac wp_bind K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etransitivity; [|apply (wp_bind K)]; simpl
+  | _ => etransitivity; [|by apply (wp_bind K)]; simpl
   end.
 Ltac wp_finish :=
   let rec go :=
@@ -44,7 +44,6 @@ Tactic Notation "wp_bin_op" ">" :=
        wp_bind K; etransitivity; [|eapply wp_bin_op; reflexivity]; wp_finish
     end)
   end.
-
 Tactic Notation "wp_bin_op" := wp_bin_op>; wp_strip_later.
 Tactic Notation "wp_un_op" ">" :=
   match goal with