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
Janno
iris-coq
Commits
de11579b
Commit
de11579b
authored
Sep 15, 2017
by
Robbert Krebbers
Browse files
Merge branch 'master' into 'master'
Fix typo in is_lock_proper for heap_lang. See merge request !57
parents
f96a894b
15c2d1ce
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/heap_lang/lib/lock.v
View file @
de11579b
...
...
@@ -34,6 +34,6 @@ Arguments locked {_ _} _ _.
Existing
Instances
is_lock_ne
is_lock_persistent
locked_timeless
.
Instance
is_lock_proper
Σ
`
{!
heapG
Σ
}
(
L
:
lock
Σ
)
N
lk
R
:
Proper
((
≡
)
==>
(
≡
))
(
is_lock
L
N
lk
R
)
:
=
ne_proper
_
.
Instance
is_lock_proper
Σ
`
{!
heapG
Σ
}
(
L
:
lock
Σ
)
N
γ
lk
:
Proper
((
≡
)
==>
(
≡
))
(
is_lock
L
N
γ
lk
)
:
=
ne_proper
_
.
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