Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joshua Yanovski
iris-coq
Commits
aedabcc3
Commit
aedabcc3
authored
Mar 22, 2017
by
Ralf Jung
Browse files
make solve_to_val work when there are still locks in the goal
parent
2e2e756b
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/tactics.v
View file @
aedabcc3
...
...
@@ -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
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment