diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 044b893d98f0cf55a5662697fb0fd0cdd5b48d89..bf81b68a1a8eb51060fbfdde240294ce360775fd 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -213,7 +213,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; unfold W.to_expr; reflexivity
+     apply W.to_val_Some; simpl; unfold W.to_expr; unlock; 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