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
Pierre-Marie Pédrot
Iris
Commits
73997f27
Commit
73997f27
authored
Apr 13, 2016
by
Ralf Jung
Browse files
Make it compile with ssreflect master
parent
c1fb1a06
Changes
1
Hide whitespace changes
Inline
Side-by-side
tests/heap_lang.v
View file @
73997f27
...
...
@@ -70,6 +70,6 @@ Section ClosedProofs.
Proof
.
iProof
.
iIntros
"! Hσ"
.
iPvs
(
heap_alloc
nroot
)
"Hσ"
as
{
h
}
"[? _]"
;
first
by
rewrite
nclose_nroot
.
by
iApply
heap_e_spec
;
first
by
rewrite
nclose_nroot
.
iApply
heap_e_spec
;
last
done
;
by
rewrite
nclose_nroot
.
Qed
.
End
ClosedProofs
.
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