Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Jonas Kastberg
iris
Commits
1595e35f
Commit
1595e35f
authored
Apr 02, 2019
by
Janno
Committed by
Robbert Krebbers
Apr 27, 2019
Browse files
Avoid conversion after only reducing goal.
parent
d5b0ff9a
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/proofmode/reduction.v
View file @
1595e35f
...
...
@@ -20,7 +20,7 @@ Declare Reduction pm_eval := cbv [
Ltac
pm_eval
t
:
=
eval
pm_eval
in
t
.
Ltac
pm_reduce
:
=
match
goal
with
|-
?u
=>
let
v
:
=
pm_eval
u
in
c
hange
v
end
.
match
goal
with
|-
?u
=>
let
v
:
=
pm_eval
u
in
c
onvert_concl_no_check
v
end
.
Ltac
pm_reflexivity
:
=
pm_reduce
;
exact
eq_refl
.
(** Called by many tactics for redexes that are created by instantiation.
...
...
@@ -34,4 +34,4 @@ Declare Reduction pm_prettify := cbn [
bi_tforall
bi_texist
].
Ltac
pm_prettify
:
=
match
goal
with
|-
?u
=>
let
v
:
=
eval
pm_prettify
in
u
in
c
hange
v
end
.
match
goal
with
|-
?u
=>
let
v
:
=
eval
pm_prettify
in
u
in
c
onvert_concl_no_check
v
end
.
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a 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