diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index f2206fed09fa7e2c3816b07d9c6d719206da2430..6ac1972a7f27d3559d905ab89d8c9c15dc6a941d 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -206,7 +206,7 @@ Ltac solve_to_val :=
   match goal with
   | |- to_val ?e = Some ?v =>
      let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
-     apply W.to_val_Some; simpl; reflexivity
+     apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
   | |- is_Some (to_val ?e) =>
      let e' := W.of_expr e in change (is_Some (to_val (W.to_expr e')));
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
@@ -227,7 +227,7 @@ Hint Extern 0 (language.atomic _) => solve_atomic : fsaV.
 
 (** Substitution *)
 Ltac simpl_subst :=
-  csimpl;
+  simpl;
   repeat match goal with
   | |- context [subst ?x ?er ?e] =>
       let er' := W.of_expr er in let e' := W.of_expr e in
diff --git a/tests/list_reverse.v b/tests/list_reverse.v
index 647aa67492034e374d1ab239ac311fa8e3f714be..680c02a6f0e9c38ba337c52e485ba311c4d88f7a 100644
--- a/tests/list_reverse.v
+++ b/tests/list_reverse.v
@@ -32,7 +32,7 @@ Lemma rev_acc_wp hd acc xs ys (Φ : val → iProp) :
   ⊢ WP rev hd acc {{ Φ }}.
 Proof.
   iIntros "(#Hh & Hxs & Hys & HΦ)".
-  iLöb (hd acc xs ys Φ) as "IH". wp_rec; wp_let.
+  iLöb (hd acc xs ys Φ) as "IH". wp_rec. wp_let.
   destruct xs as [|x xs]; iSimplifyEq.
   - wp_match. by iApply "HΦ".
   - iDestruct "Hxs" as (l hd') "(% & Hx & Hxs)"; iSimplifyEq.