From aedabcc35b48aec4be9fe1d0afb75fc36194f9e9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 22 Mar 2017 14:22:06 +0100
Subject: [PATCH] make solve_to_val work when there are still locks in the goal
---
theories/heap_lang/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index 044b893d9..bf81b68a1 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
--
GitLab