diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 1ec6d231aa5ca96186f9583f6d78eb185c7fcd9f..e984004884d7a6f1472753fdc0c64c9eb127f924 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; [|by apply later_intro]
+  | |- _ ⊑ ▷ _ => etransitivity; [|solve [ apply later_intro] ]
   end.
 Ltac wp_bind K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etransitivity; [|by apply (wp_bind K)]; simpl
+  | _ => etransitivity; [|solve [ apply (wp_bind K) ]]; simpl
   end.
 Ltac wp_finish :=
   let rec go :=