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
Iris
Iris
Commits
35c154c4
Commit
35c154c4
authored
Feb 18, 2016
by
Ralf Jung
Browse files
barrier: follow new variable name conventions
parent
035f0b29
Changes
1
Hide whitespace changes
Inline
Side-by-side
barrier/barrier.v
View file @
35c154c4
...
...
@@ -103,8 +103,8 @@ Section proof.
Local
Notation
iProp
:
=
(
iPropG
heap_lang
Σ
).
Definition
waiting
(
P
:
iProp
)
(
I
:
gset
gname
)
:
iProp
:
=
(
∃
R
:
gname
→
iProp
,
▷
(
P
-
★
Π★
{
set
I
}
(
λ
i
,
R
i
))
★
Π★
{
set
I
}
(
λ
i
,
saved_prop_own
i
(
R
i
)))%
I
.
(
∃
Ψ
:
gname
→
iProp
,
▷
(
P
-
★
Π★
{
set
I
}
(
λ
i
,
Ψ
i
))
★
Π★
{
set
I
}
(
λ
i
,
saved_prop_own
i
(
Ψ
i
)))%
I
.
Definition
ress
(
I
:
gset
gname
)
:
iProp
:
=
(
Π★
{
set
I
}
(
λ
i
,
∃
R
,
saved_prop_own
i
R
★
▷
R
))%
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