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
Tej Chajed
iris
Commits
c95907b9
Commit
c95907b9
authored
Sep 27, 2017
by
Robbert Krebbers
Browse files
Simplify solve_to_val.
parent
7ed067a9
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/tactics.v
View file @
c95907b9
...
...
@@ -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
...
...
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