diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 97a7b0a7a02bf1eb9f8178f2c1747fd7cdc8f242..37af82a7d7820a273a83f869cf901395f2f4b4e7 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -210,6 +210,7 @@ Ltac solve_closed :=
 Hint Extern 0 (Closed _ _) => solve_closed : typeclass_instances.
 
 Ltac solve_to_val :=
+  rewrite /IntoVal;
   try match goal with
   | |- context E [language.to_val ?e] =>
      let X := context E [to_val e] in change X
@@ -218,9 +219,6 @@ Ltac solve_to_val :=
   | |- 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; unfold W.to_expr; reflexivity
-  | |- IntoVal ?e ?v =>
-     let e' := W.of_expr e in change (to_val (W.to_expr e') = Some v);
-     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